______________________________________ lub(a,b)=c .congruent. a .sub.L c 
      and b .congruent..sub.L c and not .E-backward. d .di-elect cons. S.sub.L 
      : ›a .sub.L d and b .sub.L d and d .sub.L c!. glb(a,b)=c .congruent. c .sub.L 
      a and c .sub.L b and not .E-backward. d .di-elect cons. S.sub.L : ›d .sub.L 
      a and d .sub.L b and c .sub.L d! ______________________________________ 
      

      

      There exists a distinguished states "start" and "end" defined as 

      

      start(L)=.A-inverted. s .di-elect cons.L:glb(s,start)=start, 

      

      end(L)=.A-inverted. s .di-elect cons.L:lub(s,end)=end. 

      

      Since time flows downward in interval graphs, the start state (which is 
      the greatest lower bound of every state in the interval) is actually at 
      the top of the graph. Conversely, the end state is at the bottom of the 
      graph. 

      

      Construction of a lattice state graph is the act of computing. At the end, 
      the values bound to variables are the results. State lattices may be hierarchically 
      structured and composed. 

      

      FIG. 6 is a simple temporal lattice. In this case the lattice, L, is composed 
      of states S.sub.L ={s,t,u,v,w,x}, (reference numbers 310, 311, 312, 313, 
      314, and 315 respectively) and state transitions T.sub.L ={(s,t), (s,v), 
      (t,u), (v,w), (u,x), (w,x)}, (reference numbers 316, 317, 318, 319, 320, 
      and 321). The partial order relation L corresponds to the notion of before. 
      State s, 310, occurs before state w, 314, sL w, because state transitions 
      t.sub.1 =(s,v) 317 and t.sub.2 =(v,w) 319 are in T.sub.L. The transitions 
      form a chain from s 310 to w 314. Least upper bound (lub) and greatest lower 
      bound (glb) are defined for all pairs of nodes. For example, the lub of 
      u 312, and v 313 is node x 315. Similarly the glb of u 312, and v 313 is 
      node s 310. The distinguished states start(L) and end(L) are s 310 and x 
      315. 

      

      Being a "partial" order provides opportunities for parallelism. Since neither 
      u.sub.L w nor W.sub.L u, the transitions (t,u) 318, and (v,w) 319 may occur 
      independently, even simultaneously. Good DANCE programs create execution 
      lattices that are short and broad. 

      

      Temporal Meaning 

      

      Let I denote the set of all possible intervals. Consider an arbitrary interval 
      iI, composed of a lattice of states with distinguished states start(i) 101 
      and end(i) 102 with intermediate states 103 and state transitions 307 as 
      depicted in FIG. 7. 

      

      In defining meaning for DANCE language constructs over interval will be 
      denoted by a capital M subscripted with an interval or state designator, 
      the language construct in double brackets, ›› !!, the equality-by-definition 
      symbol, .tbd., followed by some expression as to the meaning of the construct: 
      

      

      M.sub.interval ››construct!!.tbd.definition 

      

      Meaning of Variables 

      

      The meaning of variable names is defined by: 

      

      .sub.j ››X!!=.sub.s ››X!! where X is a variable name, X.di-elect cons.s, 
      and s.di-elect cons.S.sub.1. 

      

      This says "the meaning of X for the interval, i, is defined as the value 
      of X in each state, s, in the interval." If X is not a state variable of 
      s, or s is not a state in the interval i, then X's meaning is undefined. 
      

      

      Meaning of Functions 

      

      Where f is a function name and e.sub.1, . . . , e.sub.k are expressions 
      or variable names, the meaning of function symbol, f, is defined by: 

      

      .sub.i ››f(e.sub.1, . . . , e.sub.k)!!=.sub.i ››f!! (.sub.i ››e.sub.1 !!, 
      . . . , .sub.i ››e.sub.k !!) 

      

      This says "the meaning of an expression in the interval (i) is the meaning 
      of the function symbol (f) applied to the meaning of each of the subexpressions 
      f uses as its operands." 

      

      DANCE grammar for functions: 

      

      ::="("+")" 

      

      ::= 
      

      

      ::="FUNCTION" "("›.sup.+ ":"!.sup.+ ")" "RETURN" ("IS" )";" 

      

      Meaning of Temporal Predicates 

      

      Where p is a temporal predicate name (i.e. a procedure name) and e.sub.1, 
      . . . , e.sub.k are expressions: 

      

      .sub.i ››p(e.sub.1, . . . , e.sub.k)!!=.sub.i ››p!!(.sub.i ››e.sub.1 !!, 
      . . . , .sub.i ››e.sub.k !!) 

      

      This says "the meaning of a temporal predicate in the interval (i) is the 
      meaning of the predicate symbol (p) in the interval applied to the meaning 
      of each of the subexpressions p uses as its operands." 

      

      Simple DANCE grammar for procedures: 

      

      ::="(" .sup.+ ")" 

      

      ::="PROCEDURE" "(" ›.sup.+ ":" !.sup.+ ")" ("IS" )";" 

      

      Temporal Formulas 

      

      Formulas are compositions of temporal predicates. Such compositions will 
      be covered in the later sections. For now consider that a formula is a simple 
      temporal predicate. 

      

      A formula w is satisfied by an interval i iff the meaning of w on i is true 
      : 

      

      :››w!!=true. 

      

      "iff" means "if and only if". 

      

      Execution of a program constructs an interval so that the interval satisfies 
      the formula that expresses the program. If all intervals satisfy a formula 
      that formula is deemed valid. However, valid formulas (tautologies) are 
      rather uninteresting programs. Constructing an interval, a lattice of states, 
      is the execution of the program. The predicates in interval temporal logic 
      become commands in DANCE; they affect side effects. 

      

      The simplest temporal formula (and the first one to be defined) is "skip."The 
      predicate "skip" is always true. 

      

      .sub.1 ››SKIP!!=true. 

      

      Simple DANCE grammar for skip temporal formula: 

      

      ::="SKIP" 

      

      Sequential Composition 

      

      Moszkowski emphasizes about his "chop" operator. It is simply a sequential 
      composition indicated by semicolon: 

      

      w.sub.1 ; w.sub.2 

      

      where w.sub.1 and w.sub.2 are formulas means 

      

      .sub.i ››w.sub.1 ; w.sub.2 !!=true iff 

      

      .E-backward.j,k:j.OR right.l and k.OR right.i: (.sub.j ››w.sub.1 !!=true) 
      and (.sub.k ››w.sub.2 !!=true) and (end(j)=start(k)) 

      

      This says "the meaning of w.sub.1 ; w.sub.2 is true in the interval i if-and-only-if 
      there exists some subintervals of i, namely j and k, such that the meaning 
      of w.sub.1 is true during j and the meaning of w.sub.2 is true during k, 
      and k starts at the end of j." Fig. 8 depicts sequential composition of 
      intervals. 

      

      Note that the two subintervals of i share the state end(j)=start(k), and 
      w.sub.1 is true on the first part of the interval and w.sub.2 is true on 
      the last part. 

      

      Simple DANCE grammar for sequential composition: 

      

      ::=";"  

      

      Parallel Composition 

      

      Conjunction of formulae provides the parallelism of DANCE: 

      

      w.sub.1 & w.sub.2 

      

      where w.sub.1 and w.sub.2 are formulas means 

      

      .sub.i ››w.sub.1 & w.sub.2 !!=true iff 

      

      there exist two subintervals of i, j.OR right.i and k.OR right.i, such that 
      

      

      .sub.j ››w.sub.1 !!=true, .sub.k ››w.sub.2 !!=true, 

      

      start(j)=start(k)=start(i), and end(j)=end(k)=end(i). 

      

      This says "the meaning of w.sub.1 & w.sub.2 over the interval i is true 
      if-and-only-if the meaning of w.sub.1 is true over some path of states, 
      j, from start(i) to end(i) in the interval i and the meaning of w.sub.2 
      is concurrently true over some different path, k, of states from start(i) 
      to end(i) in the interval i." 

      

      Where w.sub.1 is true on  ad w.sub.2 is true on  as in FIG. 
      9. Therefore w.sub.1 & w.sub.2 is true over the whole interval. 

      

      Moszkowski doesn't recognize such bifurcation. Rather he uses the more traditional 
      arbitrary interleaving of states. Though he makes reference to parallel 
      computing, his intervals are always sequences, it's just that several predicates 
      must be true over the same sequence of states. In this example the states 
      v, and w contain variables seen only by w.sub.1. Similarly the states t 
      and u contain variables seen only by w.sub.2. This is the essential, paradigmatic 
      difference in DANCE from other models. Thus the importance of local variables 
      and limited scoping in DANCE provided by domains. 

      

      Simple DANCE grammar for parallel composition: 

      

      ::="&"  

      

      Temporal Existential Quantification 

      

      For many computations additional, local variables are needed. Temporal Existential 
      quantification allows introduction of such local variables whose scope is 
      limited. The keyword DECLARE (instead of .E-backward.) introduces such variables 
      as in: 

      

      DECLARE X=c begin w end 

      

      where X is any variable, c is a constant, and w is a formula in which X 
      occurs free. 

      

      .sub.i ››DECLARE X=c begin w end!!=true iff 

      

      .sub.start(1) ››X!!=c, and .sub.1 ››w!!=true. 

      

      The definition of "free variable" is formally quite complex. Suffice to 
      say that variable X is free in formula w iff X occurs in w and nowhere else. 
      The scoping rules of DANCE are more permissive however. Even if X is used 
      outside of the existential quantifier, within w all uses of X refer to the 
      local variable. DANCE uses a syntax similar to Ada; the predicate above 
      comes from the Ada production . Existential quantification provides 
      scoping within the model of computation. Variables introduced in the declaration 
      part of blocks, procedures, and packages (implicitly) invoke existential 
      quantification over their scope. Existential quantification readily generalizes 
      to many variables. Later, we will require such existentially quantified 
      variables to have type declarations. 

      

      Simple DANCE grammar for existential quantification: 

      

      ::="DECLARE" ›":" ("=" )!.sup.+ 
      "BEGIN"  "END" 

      

      Temporal Bounded Universal Quantification 

      

      Bounded universal quantification allows a group of formulae to be executed 
      together, but with different parameters. The keyword FORALL is used instead 
      of .A-inverted.. 

      

      FORALL X IN b DO w 

      

      where X is any variable, b is a boolean expression or range, and w is a 
      formula means: 

      

      (DECLARE X=x.sub.1 begin w end) & (DECLARE X=x.sub.2 begin w end) & . . 
      . & (DECLARE X=x.sub.n begin w end) 

      

      where x.sub.1, x.sub.2, . . . , x.sub.n are values for X that make b true. 
      For now consider b to be a subrange of integers such as 0.ltoreq.X.ltoreq.12, 
      which would initiate twelve copies of w each having a local constant X ranging 
      from 0 to 11. 

      

      .sub.i ››FORALL X IN b DO w!!=true iff 

      

      .E-backward.n:n.gtoreq.0: 

      

      (.A-inverted. x.sub.k :1.gtoreq.k.gtoreq.n:b.sup.x.sub.xk) and (.A-inverted.y 
      :: b.sup.x.sub.y y .di-elect cons.{x.sub.1, x.sub.2, . . . , x.sub.n }) 
      and 

      

      (.E-backward.j1 . . . jn:j1.OR right.i . . . jn.OR right.i: 

      

      .sub.1 ››DECLARE X=x.sub.1 begin w end!!=true, and 

      

      .sub.2 ››DECLARE X=x.sub.2 begin w end!!=true, and . . . and 

      

      .sub.jn ››DECLARE X=x.sub.n begin w end!!=true) 

      

      Bounded universal quantification (FORALL) is the source in DANCE for massively 
      parallel processing opportunities; each subinterval can be executed concurrently. 
      FIG. 10 depicts universal quantification. 

      

      All program variables must be introduced with either existential or universal 
      quantification. A range such as ›1 . . . 10! may substitute for the boolean 
      expression, b, with the understanding that ›j . . . k! means j.ltoreq.X.ltoreq.k; 
      X takes on all the discrete values from j to k inclusive. 

      

      Simple DANCE grammar for universal quantification: 

      

      ::="FORALL" ":" "IN" ›.vertline.!"DO" 
       

      

      Assignment 

      

      So far we have no way to modify the values of state variables. Such a language 
      has limited utility| Therefore temporal assignment is needed: 

      

      X:=e 

      

      where X is a variable name and e is an expression. The value of X at the 
      end of the subinterval becomes the value of e evaluated in the state at 
      the beginning of the subinterval. Formally: 

      

      .sub.i ››X:=e!!=.sub.end(i) ››X!!=.sub.start(i) ››e!!. 

      

      This says "the meaning of X (its value) at the end of the interval i is 
      the meaning of e evaluated at the beginning of the interval i." FIG. 11 
      shows an interval satisfying an assignment formula. 

      

      Simple DANCE grammar for assignment: 

      

      ::=":="  

      

      Alternative Command 

      

      The alternative command provides data dependent branching. 

      

      .sub.i ››1F B1.gtoreq.S1 ›!B2.gtoreq.S2 ›!. . . ›!Bn.gtoreq.Sn F1!!=true 
      if f 

      

      (.sub.start(i) ››B1!!or .sub.start(i) ››B2!! or . . . or .sub.start(i) ››Bn!!) 
      and 

      

      (.sub.start(i) ››B1!!.sub.i ››S1!!) and (.sub.start(i) ››B2!!.sub.i ››S2!!) 
      and . . . and 

      

      (.sub.start(i) ››Bn!!.sub.i ››Sn!!) 

      

      Simple DANCE grammar for alternative command: 

      

      ::="IF" ".gtoreq."  

      

      ›"›!" ".gtoreq." !*"FI" 

      

      Iterative command: 

      

      The iterative command provides data dependent looping: 

      

      
    ______________________________________
    .sub.i ››DO B1 => S1  B2 => S2 .sub.1... Bn => Sn OD!! = true iff
    .E-backward.j1...jc ; j1.di-elect cons.i ... jc.OR right.i:
     (.orgate..sub.k.epsilon.›l..c! jk = i) and
     (start(i)=start(j1) and end(j1)=start(j2) and ...and
     end(jc)=end(i) ) and
     .A-inverted.k : 0<=n:
      ( (.sub.start(jk) ››B1!! .sub.jk ››S1!!) and (.sub.start(jk) ››B2!!
    .sub.jk ››S2!!)
      and ... and (.sub.start(jk) ››Bn!! .sub.jk ››Sn!!) )
    ______________________________________

      

      

      Simple DANCE grammar for iterative command: 

      

      ::="DO" ".gtoreq."  

      

      ›"›!" ".gtoreq." !* "OD" 

      

      Combinable Operations 

      

      Combinable operations are crucial to obtaining high efficiency in parallel 
      processing. Combinable operations allow access to a broad range of data 
      structures in parallel without mutual exclusion. The meaning of a fetch-add 
      (other combinable operations are similar) is that the value of a shared 
      variable is fetched (read) and its retained value is indivisibly changed 
      to the sum of its previous value and the parameter provided in the fetch-add. 
      If two (or more) processors fetch-add the same variable at the same time, 
      they receive values as if the fetch-adds occur in some sequential order, 
      even though the fetch-adds really occur at the same instant. 

      

      Previous language constructs were defined over an interval with some unspecified 
      number of intervening states between the initial state and the final state 
      (e.g. assignment). Originally I had not used the "next" (O) temporal operator, 
      but definition of combinable operations demands it. The meaning of the "next" 
      operator over an interval i is for some state s.di-elect cons.i, O(expression) 
      is true if and only if the expression is true in state t.di-elect cons.i 
      and no other state occurs between s and t. 

      

      .sub.s ››O(e)!!=true 

      

      iff 

      

      .sub.t ››e!!=true and glb(s,t)=s and lub(s,t)=t and 

      

      not (.E-backward. u.di-elect cons.i:glb(s,u)=s and lub(u,t)=t). 

      

      A single fetch-add where X is the shared variable e is the expression to 
      be added (usually an integer constant) and Y is the variable to receive 
      the fetched value is defined as follows: 

      

      .sub.s ››FETCH.sub.-- ADD(X,e,Y)!!=true 

      

      iff 

      

      .sub.s ››O(Y=X)!!=true and .sub.s ››O(X=X+e(!!=true. 

      

      Multiple combinable operations are more difficult to define. The new value 
      held by the shared variable is straightforward the new value is the sum 
      (and, or, xor) of the old value and the sum (and, or, xor) of the values 
      contained in the combinable operations. The returned values are more problematic; 
      they are the result of some, nondeterministic ordering as if they occurred 
      one at a time. The Layered network combines requests and decombines responses 
      for combinable operations. Since which processor executes a part of an interval 
      is unspecified, the apparent sequential order cannot be known. Fortunately 
      it doesn't need to be. 

      

      Let ndperm(e.sub.1, . . . , e.sub.k) be a nondeterministic permutation of 
      expressions resulting in some scrambling of their order: 

      

      .sub.i ››ndperm(e.sub.1, . . . , e.sub.k)!!=(e.sub.1s, . . . , e.sub.ks) 
      

      

      where 

      

      .A-inverted.j:1.ltoreq.j.ltoreq.k: 

      

      .E-backward.m:e.sub.m =e.sub.js and 

      

      .A-inverted.n:1.ltoreq.n.ltoreq.k, n=j:not(e.sub.m =e.sub.n). 

      

      Now with ndperm, fetch-add can be defined for simultaneous execution: 

      

      .sub.k ››FETCH.sub.-- ADD(X,e.sub.1,Y.sub.1) & FETCH.sub.-- ADD(X,e.sub.2,Y.sub.2) 
      & . . . & FETCH.sub.-- ADD(X,e.sub.k, Y.sub.k)!!=true 

      

      iff 

      

      there exists some ndperm(e.sub.1, . . . , e.sub.k)=(e.sub.1s, . . . , e.sub.ks) 
      such that 

      

      .sub.ik ››O(X=X+e.sub.1 +e.sub.2 +. . . +e.sub.k !!=true and .sub.ik ››O(Y.sub.1s 
      =X)!!=true and 

      

      .sub.ik ››O(Y.sub.2s =X+e.sub.1s)!!=true and .sub.ik ››O(Y.sub.3s =X+e.sub.1s 
      +e.sub.2s)!!=true and . . . and 

      

      .sub.ik ››O(Y.sub.ks =X+e.sub.1s +e.sub.2s +. . . +e.sub.k-1s)!!=true. 

      

      What the above expressions say is that the shared variable X gets all the 
      values contained in the fetch-ads added to it and the values returned are 
      the original X value plus some subset of other values from other fetch-adds. 
      The reason why this is important is that the behavior is as if the fetch-adds 
      occurred in some sequential order when in fact they occurred at the same 
      instant. Combinable operations are why "interleaving" of states are inappropriate. 
      Any languages or architectures for which interleaving provides an adequate 
      model are doomed to poor efficiency. 

      

      The fetch-and, fetch-or, and fetch-xor are defined similarly: 

      

      .sub.ik ››FETCH.sub.-- AND(X,e,Y)!!=true iff 

      

      .sub.ik ››O(Y=X)!!=true and .sub.ik ››O(X=X AND e)!!=true. 

      

      .sub.ik ››FETCH.sub.-- AND(X,e.sub.1,Y.sub.1) & FETCH.sub.-- AND(X,e.sub.2,Y.sub.2) 
      & . . . & FETCH.sub.-- AND(X,e.sub.k,Y.sub.k)!!=tru e 

      

      iff 

      

      there exists some ndperm(e.sub.1, . . . , e.sub.k)=(e.sub.1s, . . . , e.sub.ks) 
      such that 

      

      .sub.ik ››O(X=X AND e.sub.1 AND e.sub.2 AND . . . AND e.sub.k !!=true and 
      

      

      .sub.ik ››O(Y.sub.1s =X)!!=true and .sub.ik ››O(Y.sub.2s =X AND e.sub.1s)!!=true 
      and 

      

      .sub.ik ››O(Y.sub.3s =X AND e.sub.1s AND e.sub.2s)!!=true and . . . and 
      

      

      .sub.ik ››O(Y.sub.ks =X AND e.sub.1s AND e.sub.2s AND . . . AND e.sub.k-1s)!!. 
      

      

      .sub.ik ››FETCH.sub.-- OR(X,e,Y)!!=true iff 

      

      .sub.ik ››O(Y=X)!!=true and .sub.ik ››O(X=X OR e)!!=true. 

      

      .sub.ik ››FETCH.sub.-- AND(X,e.sub.1,Y.sub.1) & FETCH.sub.-- OR(X,e.sub.2,Y.sub.2) 
      & . . . & FETCH.sub.-- AND(X,e.sub.k,Y.sub.k)!!=true 

      

      iff 

      

      there exists some ndperm(e.sub.1, . . . , e.sub.k)=(e.sub.1s, . . . , e.sub.ks) 
      such that 

      

      .sub.ik ››O(X=X OR e.sub.1 OR e.sub.2 OR . . . OR e.sub.k !!=true and 

      

      .sub.ik ››O(Y.sub.1s =X)!!=true and .sub.ik ››O(Y.sub.2s =X OR e.sub.1s)!!=true 
      and 

      

      .sub.ik ››O(Y.sub.3s =X OR e.sub.1s OR e.sub.2s)!!=true and . . . and 

      

      .sub.ik ››O(Y.sub.ks =X OR e.sub.1s OR e.sub.2s OR . . . OR e.sub.k-1s)!!. 
      

      

      .sub.ik ››FETCH.sub.-- XOR(X,e,Y)!!=true iff 

      

      .sub.ik ››O(Y=X)!!=true and .sub.ik ››O(X=X XOR e)!!=true. 

      

      .sub.ik ››FETCH.sub.-- XOR(X,e.sub.1,Y.sub.1) & FETCH.sub.-- XOR(X,e.sub.2,Y.sub.2) 
      & . . . & FETCH.sub.--XOR(X,e.sub.k,Y.sub.k)!!=true 

      

      iff 

      

      there exists some ndperm(e.sub.1, . . . , e.sub.k)=(e.sub.1s, . . . , e.sub.ks) 
      such that 

      

      .sub.ik ››O(X=X XOR e.sub.1 XOR e.sub.2 XOR . . . XOR e.sub.k !!=true and 
      

      

      .sub.ik ››O(Y.sub.1s =X)!!=true and .sub.ik ››O(Y.sub.2s =X XOR e.sub.1s)!!=true 
      and 

      

      .sub.ik ››O(Y.sub.3s =X XOR e.sub.1s XOR e.sub.2s)!!=true and . . . and 
      

      

      .sub.ik ››O(Y.sub.ks =X XOR e.sub.1s XOR e.sub.2s XOR . . . XOR e.sub.k-1s)!!=true. 
      

      

      The swap operation behaves differently. When a single swap occurs at a time, 
      the value of the shared variable becomes the parameter of the swap and the 
      value returned is the previous shared variable value. 

      

      .sub.ik ››SWAP(X,e,Y)!!=true iff 

      

      .sub.ik ››O(Y=X)!!=true and .sub.ik ››O(X=e)!!=true. 

      

      When many swaps occur simultaneously one processor will get the value of 
      the shared variable the others will get values from some other swap, and 
      the shared variable, the others will get values from some other swap, and 
      the shared variable will get the swap value no processor receives. 

      

      .sub.ik ››SWAP(X,e.sub.1,Y.sub.1) & SWAP(X,e.sub.2,Y.sub.2) & . . . & SWAP(X,e.sub.k,Y.sub.k)!!=true 
      

      

      iff 

      

      there exists some ndperm(e.sub.1 ... e.sub.k)=(e.sub.1s, . . . , e.sub.ks) 
      such that 

      

      .sub.ik ››O(X=e.sub.ks !!=true and .sub.ik ››O(Y.sub.1s =X)!!=true and 

      

      .sub.ik ››O(Y.sub.2s =e.sub.1s)!!=true and .sub.ik ››O(Y.sub.3s =e.sub.2s)!!=true 
      

      

      and . . . and .sub.ik ››O(Y.sub.ks =e.sub.k-1s)!!=true. 

      

      The swap combinable operation is good for manipulating pointers in dynamic 
      data structures. The fetch-add is good for indexing into a shared array. 
      The fetch-and fetch-or and fetch-xor are good for clearing, setting, and 
      toggling flags respectively. Virtually all of the DANCE programs use combinable 
      operations to manipulate shared variables to access data structures in parallel 
      without mutual exclusion. Hardware support for combinable operations is 
      necessary for high efficiency. In addition to combining in the Layered network, 
      I'd like combinable operations in the processor's ISA and memory management 
      unit. Although combinable operations are expected to represent a small percentage 
      of all instructions executed, they (can) eliminate parallelism-destroying 
      mutual exclusion and blocking. 

      

      Temporal Domains 

      

      Temporal domains hold bindings between identifiers (variables) and values. 
      All state variables occur in some domain and at most one domain. Domains 
      hold not only changeable states, but complete packages which contain procedures 
      and functions as well as state variables. 

      

      Domains are essential for proving noninterference--that no other processor 
      is modifying the variables any particular processor is currently using. 
      Noninterference is crucial to showing that parallel activities can occur 
      together correctly ›"An Axiomatic Proof Technique for Parallel Programs," 
      Susan Owicki and David Gries, Acta Informatica 6, Springer-Verlag 1976!. 
      

      

      Domain Trees 

      

      All domains for a single parallel program running on a single Multitude 
      computer (which is comprised of many processors) form a rooted, directed 
      tree. Intervals being executed (causing state change) exist in some leaf 
      domain. The temporal predicates (commands) that control the interval can 
      use any variable-value bindings in any domain below it in the tree. The 
      domain tree will dynamically expand an contract as the program is executed. 
      A new domain is created when a block is entered that declares local variables 
      and is deleted when the block is exited. 

      

      Domain names are formed by a string of identifiers separated by periods 
      representing the path in the domain tree from the root to the leaf. The 
      local variables immediately declared within a subprogram are contained in 
      a domain whose name is the subprograms identifier prepended (with a period) 
      with the domain name in which it was invoked. Within subprograms, blocks 
      that declare new variables may be encountered; a new domain leaf is grown. 
      Non-nested blocks are assigned numbers starting with 1, in the order in 
      which they are encountered. Nested blocks grow new domain leaves. Automatically 
      numbered blocks cannot be confused with either named domains or subprogram 
      domains since DANCE identifiers cannot start with digits. However domain 
      identifiers and subprogram identifiers may be the same. However, an identifier's 
      position in the name make clear whether it's a domain name or subprogram 
      name. 

      

      In the following, d, d1, d2, etc. stand for domains and N(d) stands for 
      the name of domain d. Define the domain operator , by: 

      

      ››d!!={(n,v).vertline.n.di-elect cons.identifier, v.di-elect cons.Type(n)} 
      

      

      which means "the domain of d is a set of pairs in which the first element, 
      n, is a program identifier and the second element, v, is a value in the 
      type of n." Types are sets of values. A domain contains the domains of all 
      its ancestors in the domain tree. Ancestor domain names are formed by truncating 
      their descendent's names: 

      

      ››d1!!.OR right.››d2!! iff .E-backward. s:string.vertline.N(d1) && "." SSs=N(d2) 
      

      

      where && is string concatenation. That is that domain d2 call "see" all 
      the values in every domain d1 whose name is a shortened version of d2. All 
      the values visible in domain d2 are either declared in the DANCE program 
      text corresponding to d2, or are declared in some ancestor of d2. 

      

      Domains are neighbors if they have some variables they both can see: 

      

      neighbors(d1,d2)=››d1!!.andgate.››d2!!=.o slashed.. 

      

      Remote domains have no common variables: 

      

      remote(d1,d2)=››d1!!.andgate.››d2!!=.o slashed.. 

      

      Remote domains are needed to represent programs that span machine boundaries, 
      i.e. distributed processing. 

      

      Simple DANCE program fragment: 

      

      
    ______________________________________
    package body ex:example is
    declare
    A:float;
    procedure p is
    declare
    W:integer;
    begin
    command1
    end;
    procedure h is
    declare
    X:float;
    begin
    declare
            Y:bool;
    begin
            command2
    end
    command5
    ;
    declare
            Z:char;
    begin
            command3
            ;
            declare
              V:string;
            begin
              command4
            end
    end
    end;
    end package
    ______________________________________

      

      

      In the above program fragment: 

      

      command 1 sees W and A; 

      

      command 2 sees A, X, and Y; 

      

      command 3 sees A, X, and Z; 

      

      command 4 sees A, X, Z, and V; 

      

      command 5 sees X and A. 

      

      FIG. 42 shows the domains for the example above. FIG. 42 is not a set diagram 
      in the usual sense of a subset drawn inside its superset. The set of nameable 
      and therefore usable variables for a particular domain are all the variables 
      declared within the domain, union variables declared in surrounding domains. 
      Domains are necessary for proof of noninterference. The easiest way to assure 
      non-interference is by restricting access to critical variables. Semaphores 
      protect variables by serializing access to critical sections. DANCE protects 
      variables with domains. By relying on the fact that no other interval can 
      "see" critical, local variables, noninterference is assured. 

      

      Remote Procedure Call 

      

      Distributed systems have domains that do not form a tree--no single domain 
      exists within which all other domains are contained. No shared address space, 
      no combinable operations, just messages, usually point-to-point sans confirmation. 
      Remote procedure call (RPC) works just fine for much of what one would like 
      to do at disparate geographical locations. (Note: I explicitly reject message 
      passing paradigms for parallel processing that have one machine out of many 
      microprocessors, in a single location. Only geography demands distribution.) 
      

      

      However there are worthwhile applications that demand geographical distribution 
      that cannot utilize nested RPCs such as databases. RPCs are great for computation 
      where the duration or lifetime of the domain which contains all accessed 
      variables coincides with the duration of the invoked procedure. Such applications 
      abound, i.e. photorealistic, 3D, animated rendering. 

      

      Sometimes the lifetime of state variables must exceed the lifetime of any 
      procedure that uses it. Databases are like this. The traditional means of 
      ensuring noninterference (and thus partial correctness) is with locks, semaphores, 
      monitors or some other form of mutual exclusion which may lead to deadlock. 
      This has caused a colorful consideration of resource allocation and deadlock 
      detection starting with Dijkstra's dining philosophers and ending with global 
      snapshots. Total correctness proofs cannot tolerate even the possibility 
      of a deadlock occurring--the program must terminate| How to ensure noninterference 
      between transactions that may wish to exclusively use the same values without 
      risking deadlock? 

      

      Must have noninterference cannot permit deadlock. Noninterference without 
      deadlock. But how? 

      

      1) Divide the database into a large number of domains which may reside on 
      machines across the country. 

      

      2) Impose a total ordering on the domains. 

      

      3) Allow only one RPC to be active in a domain--queue other received RLPC 
      invocations first-in-first-out. 

      

      4) Make database accesses that need to maintain consistency between values 
      in different domains use an RPC chain in the order of the domains used. 
      

      

      The proof by induction of totally correct programs that invoke only other 
      (already proven) totally correct subprograms with RPC is direct. Anything 
      that is totally correct and is invoked with RPC will eventually terminate 
      and return with the right value, and the caller will then terminate (the 
      inductive hypothesis). The chains of RPCs that may occur must be finite 
      so that the deepest invocation will terminate without making further invocations 
      (the basis). 

      

      An RPC chain is a finite number of nested RPC calls each of which can be 
      on a different machine. During the invocation phase, values of the database 
      domains of interest are "read." During the return phase, values of the database 
      are "written." Therefore any mapping from previous database values to new 
      values is possible, and provide some initiating transaction the answer to, 
      and confirmation of, its query. 

      

      The total ordering of domains makes it work. Suppose a single transaction 
      occurs. It will create a chain through the database complete its last RPC 
      and eventually terminate. If a transaction is stalled because its deepest 
      RPC is stalled in a queue at a domain already in use, it will eventually 
      be given access since the currently active RPC (and all RPCs ahead in the 
      queue) will eventually terminate and release the domain (the inductive hypothesis). 
      There is some "deepest" chain that occupies (has an active RPC chain) in 
      the highest numbered domain. It will eventually terminate and release all 
      its domains therefore possibly unblocking other RPC chains (the basis). 
      Therefore all RPC chains will eventually terminate and total correctness 
      can be proven. 

      

      This method only works efficiently when the transactions require domains 
      evenly--each processor must know in which domain the value of interest lies. 
      Tree-structured directories save much space and may work well for sequential 
      accesses, but they cause "hot spots" that would substantially degrade the 
      performance when distributed. On the other hand, if the number of domains 
      were large enough so that the probability of any two transactions needing 
      the same domain were small, the system would exhibit latency largely independent 
      of the number of transactions--a blessing to travel agents worldwide. 

      

      Type Theory 

      

      Type systems are important. Most languages such as Pascal and C only allow 
      types that are basic and constructed. Basic types generally correspond to 
      types supported directly by the hardware like integers, floating point number 
      and characters. Constructed types are built from the basic types to form 
      arrays, lists, and records. Some languages such as Ada allow forms of polymorphism 
      (many types) through operator overloading. Abstract data typing seemed to 
      answer a desire for powerful, reusable, and encapsulated types. A paper 
      by Cardelli and Wegner ›"On Understanding Types, Data Abstraction, and Polymorphism," 
      Luca Cardelli and Peter Wegner, Computing Surveys, Vol. 17, No. 4, December 
      1985.! gave new vistas to my thinking about types. The type system of DANCE 
      has been adapted from Cardelli and Wegner's type expression language Fun. 
      Existentially and universally quantified types are realized through "packages" 
      described in a following section. 

      

      Basic Types 

      

      The basic types of DANCE are: 

      

      Integer, Bool, Rat, Float, and Char 

      

      short for integer, boolean, rational, floating point, and character. Rational 
      is included because exactness cannot be obtained with floating point numbers. 
      A special value, NIL, is a member of each of the basic types representing 
      no value. Uninitialized variables have the value NIL. Attempts to use variables 
      whose values are NIL in expressions will result in error messages. However 
      NIL can be assigned to variables. 

      

      Simple DANCE grammar for simple types: 

      

      ;;="INTEGER".vertline."BOOL".vertline."RAT".vertline."FLOAT".vertline 
      ."CHAR" 

      

      Constructed Types 

      

      Types may be constructed from basic types by the use of type expressions. 
      Arrays, function spaces, records, and variant types may be constructed. 
      Arrays are integer indexed and behave like functions as in ›The Science 
      of Programming, David Gries, Springer-Verlag, 1981!. Accessing an array 
      with an index out of bounds results in NIL. Functions are first-class and 
      so may be passed as parameters. Record and variant types have standard usages. 
      

      

      Simple DANCE grammar for constructed types: 

      

      
    ______________________________________
     ::= "(" ›+ .vertline. +!")"
     ::= "ARRAY" "›" + "!" "OF" 
     ::=  "=>" 
     ::= "RECORD"  ":"  ›","  ":" !8
    "END" "RECORD"
     ::= "VARIANT"  :  ";"
     ":"  ›","  ":" !* "END" "VARIANT"
    ______________________________________

      

      

      Parametric Types 

      

      Parametric types are type constructors that take type parameters to build 
      a new type. 

      

      For example, a generic list could be defined and then specialized as with: 
      

      

      
    ______________________________________
    TYPE List›Item! IS --declare a generic list
    VARIANT c: empty, cons;
    empty: NIL,
    cons: RECORD
    head: Item,
    tail : List›Item!
    END RECORD
    END VARIANT;
    TYPE IntList : List›Integer!;
    bind Integer to item to get IntLst
    ______________________________________

      

      

      Simple DANCE grammar for parametric types: 

      

      
    ______________________________________
     ::= "TYPE"  ( "›" .sup.+
     "!" )
    "IS"  ";"
     ::=  "›" .sup.+ "!"
    ______________________________________

      

      

      Packages are Abstract Data Types 

      

      Packages provide program structuring and information hiding. The packages 
      in DANCE are adapted from those in ›Algebraic Specifications in Software 
      Engineering. Ivo Van Horebeek & Johan Lewi, Springer-Verlag, 1989! and inspired 
      by packages in Ada ›ANSI/MIL-STD-1815A-1983 Reference Manula for the Ada 
      Programming Language. American National Standard Institute, 1983.!. 

      

      Packages have two parts: a visible, declaration section, and a hidden body. 
      The body is lot really hidden or secret, just that it is not within the 
      scope that can be seen by other packages. All that a programmer should need 
      to know about the services of a package should be visible in the declaration 
      section. 

      

      Those familiar with object oriented languages like Smalltalk will recognize 
      that packages define classes and that these classes are instantiated as 
      objects. Such considerations will be finessed for the time being. The conception 
      of executing a package body is adequate. 

      

      Packages have names. The items within a package can be named from other 
      packages similar to records by prefacing the name of the item with the package's 
      name and a period. Packages group together objects and operations that have 
      useful purpose. Packages require lots of declarations. C hackers don't want 
      to be bothered with scoping more sophisticated than "local" and "global." 
      DANCE adds some powerful, yet esoteric declarations to Ada's. These declarations 
      allow generic (polymorphic) programs that are parameterized with type (universal 
      type quantification) and certain requirements for the awaited type (inheritance 
      via bounded universal quantification). Ada's private type declarations serve 
      as existential type quantification. DANCE's type system (including pointers 
      or access types) allows definition of every type in either Ada or Fun, plus 
      exotic types not found in either. 

      

      A requirement clause demands passing of a type to tie package. Often this 
      type will be restricted to some form. Cardelli and Wegner's bounded universal 
      quantification is realized through the use of requirement clauses. 

      

      An import clause specifies the use of another package's services. Such packages 
      must be visible at compile time. 

      

      The private type declaration declares types that are defined within the 
      package but may be used by other packages. The implementation of the types 
      (and operations using such types) are hidden within the body of the package. 
      This corresponds to Cadlelli & Wegner's existential quantification. The 
      private type states that a type exists but does not tell how it works. Other 
      packages may only manipulate existentially quantified types with operations 
      declared by the package. 

      

      The package body contains the implementations of the operations. The relationships 
      between each section will become clearer with later examples. 

      

      Simple DANCE grammar for packages: 

      

      
    __________________________________________________________________________
     ::=  .vertline. 
     ::= "PACKAGE"  ( "›" + "!" ) "IS"
    *
    *
    .sup.+  ( "PRIVATE" .sup.+) "END" "PACKAGE"
     ::= "PACKAGE BODY"  ":"  "IS"
    .sup.+  "END" "PACKAGE"
     ::= "PROCEDURE"  "(" ›.sup.+
    ":" !