UNITY (programming language)
The programming language UNITY was constructed by K. Mani Chandy and Jayadev Misra for their book Parallel Program Design: A Foundation. It is a rather theoretical language, which tries to focuse on what, and not where, when or how. The peculiar thing about the language is that it has now flow control. The statements in the program run in a random order, until none of the statements any longer may cause change if run. A correct program converges into a fix-point.
All statements are assignments, and are separated by #
. A statement can consist of multiple assignments, on the form a,b,c := x,y,z
, or a := x || b := y || c := z
. You can also have a quantified statement list, for example <# x,y : 0 < x < y < n :: statement>
, where x and y are chosen randomly among the values that satisfy the quantification. A quantified assignment is similar. In <|| x,y : 0 < x < y < n :: statement >
, the statement is executed simultaneously for all
x
and y
satisfying 0 > x > y < n
.
Examples
Randomsort
Random sort the array by randomly choosing chosing two numbers, and swap them if they are in the wrong order. Using expected exponential time, one processor and expected exponential work.
Program sort
declare
n: integer,
A: array [0..n-1] of integer
initially
n = 20 #
<# i : 0 <= i and i < n :: A[i] = rand() % 100 >
assign
<# i,j : 0 <= i < n and 0 <= j < n ::
A[i], A[j] := A[j], A[i] if i < j and A[i] > A[j] >
end
Insertionsort
Insertion sort the array by comparing adjacent numbers, and swapping them if they are in the wrong order. Using time, processors and work.
Program sort2
declare
n: integer,
A: array [0..n-1] of integer
initially
n = 20 #
<# i : 0 <= i and i < n :: A[i] = rand() % 100 >
assign
<# k : 0 <= k < 2 ::
<|| i : i % 2 = k and 0 <= i < n - 1 ::
A[i], A[i+1] := A[i+1], A[i] if A[i] > A[i+1] > >
end
Mergesort
Merge sort the array using a constant time merge. Using time, processors and work. In this example, a value may be written many times simultaneously, since we are not carefull with the <=
operator. If you expand the a,b
quantification, you can get CREW PRAM complexity.
Program sort3
declare
n,m: integer,
A,S,N: array [0..n-1] of integer
initially
n = 20 #
m = n ||
<|| i : 0 <= i and i < n :: A[i], N[i], S[i] = rand()%100, 1, i >
assign
<|| s : 0 <= s < m - 1 and s % 2 = 0 ::
<|| a,b : (a = 0 and b = 1) or (a = 1 and b = 0) ::
<|| sa : 0 <= sa < N[s+a] ::
A[S[s]+sa] := A[S[s+a]+sa]
if A[S[s+a]+sa] <= A[S[s+b]] ||
<|| sb : 0 < sb < N[s+b] ::
A[S[s]+sa+sb] := A[S[s+a]+sa]
if A[S[s+b]+sb-1] <= A[S[s+a]+sa] <= A[S[s+b]+sb] > ||
A[S[s]+sa+N[s+b]] := A[S[s+a]+sa]
if A[S[s+b]+N[s+b]-1] <= A[S[s+a]+sa] > > ||
S[s/2] := S[s] ||
N[s/2] := N[s] + N[s+1] > ||
S[(m-1)/2], N[(m-1)/2] := S[m-1], N[m-1] if m%2 = 1 ||
m := m/2 + m%2
end
References
- K. Mani Chandy and Jayadev Misra (1988) Parallel Program Design: A Foundation.