以同態建造平行程式

Abstract

平行程式在現今的世界中佔有非常重要的份量。但是,如何開發平行程式 卻不是件簡單的事情。傳統上,為了開發平行程式,程式設計師習慣也必須將 現有的序列化程式重新改寫成平行的版本。但是,這樣做卻需要花費額外的成 本與時間。自然地,程式設計師會想要有一套自動化的方法可以讓他們不必為 了平行化而重新實作同一套演算法。因此,大量的研究試圖去開發出有效的方 法,以自動化地從現有的序列化程式開始建構或合成出平行程式。其中一種可 行的方法就是採用程式推導(program derivation)來做為平行化程式的技術基礎。 程式推導允許程式設計師從程式的規格,或是現有的程式定義與性質,來推導 並建構出滿足目標需求的程式定義。 ! 本研究中,我們使用同態來描述平行程式的性質並且專注在串列處理相關 的程式。我們以兩種不同的特化實例來加以定義:串列同態(list- homomorphism),用以描述處理平行串列歸納(list-reducing)的程式;串列反同 態(list-unhomomorphism),用以描述處理平行串列生成(list-generating)的程式。 第三串列同態定理(third list-homomorphism theorem)告訴我們:一個程式如果 具有雙摺疊性(bi-foldability),則必然存在一個運算子使得該程式可以被寫成 一個串列同態。經由利用第三串列同態定理,我們推廣並總結出兩種可以由序 列化串列歸納程式推導出其平行定義的方法。第一種允許我們將雙摺疊性之證 明一般化成串列同態之證明,而其中則包含了目標程式之串列同態定義。第二 種方法允許我們經由語法操作而產生出目標串列同態之定義,一旦目標程式之 右弱反函數(right weak inverse)可以被設計並決定。另一方面,對於串列反同 態,我們推廣出一個第三串列同態定理之對偶定理(dual theorem)。基於此定 理,如果某兩個串列反同態之基本性質之前提條件皆可以被滿足的話,我們可 以根據序列化串列生成程式之定義建構出一個串列反同態之定義。

Parallel programming plays an very important role in nowadays world. To develop a parallel program, however, is not a simple task. Traditionally programmers are used to and have to rewrite a sequential program to its parallel version. This, however, takes lots of extra efforts and times. It natural that programmers want to have an automatic method for saving themselves from re-implementing the same algorithm twice. Therefore plenty of previous works have tried to develop methods for constructing and synthesising parallel programs from existing sequential programs. One of potential ways is using program derivation which allows us to construct a program definition from its specification, or, in this case, from existing definitions and properties. In this thesis, we use homomorphism as a model of parallel programs and focus on programs that handle the well-known linear data structure, list. We realise homomorphism as two specialisations: the list-homomorphism, which works as properties and is used for modelling parallel list-reducing programs; and the list- unhomomorphism, for parallel list-generating programs. By taking advantage of the third list-homomorphism theorem we introduce two methods to derive parallel list- reducing programs from its sequential definitions. The first method allows us to transform a proof of bi-foldability to a proof of existing of list-homomorphism where, obviously, contains the definition of list-homomorphism itself. The second one, provides us a syntactical approach to construct a list-homomorphism once an right weak inverse of the program we want to parallelise can be designed and picked. For list- unhomomorphism, on the other hand, we develop a dual theorem of the third list- homomorphism theorem so that list-generating programs can be constructed from its sequential definitions once the sufficient conditions of two essential properties of list- unhomomorphism can be satisfied.