These html pages are based on the PhD thesis "Cluster-Based Parallelization of Simulations on Dynamically Adaptive Grids and Dynamic Resource Management" by Martin Schreiber.
There is also more information and a PDF version available.

4.7 Verification of stack-based edge communication

This section gives a formal proof of a valid edge-oriented communication between cells with the stack system using push and pop operations for the Sierpiński SFC. Using push operations on edges of type new and pop operations on edges of type old, the following theorem holds:

Theorem 4.7.1 (Valid stack-based communication) Using the communication schemes with the pop and push operations on the communication stack yields correct data transfer to each cell adjacent to the corresponding edge.


The proof of the theorem is supported by axiomatic rules closely related to those of the Hoare calculus [Hoa69]. We define inference rules given in the form AB- with A stating the condition which has to hold true and B the condition to replace A. The conditions are given by a tuple of tuples {{P}S{Q}}n with the precondition P, the code-statement S and the postcondition Q.

We further assume push and pop operations specified via push(S,a), pushing the element a to stack S, and pop(S,a) fetching element a from the stack.

The push and pop operations are extended with the pre- and postconditions

         {Sk }  push(Sk,α ) {Sk =  (s1,s2,...,s k ,α )},
   k  k               k        k    k  k      |Sk |                 (4.14)
{S  ,S |Sk| = β } pop(S  ,β)  {S  =  (s1,s2,...,s|Sk|-1)}.
with the superscript k generating a unique labeling of the stacks.
Reduction and commutative rules

Correct communication: The success of a correct pop operation by applying the grammar and inheritance of types lead to pop operations pop(S,α), testing for correct fetching of element α from the top of the stack. This leads to the rule

           k            k      k    k  k      k
R6 : ----{S|Sk| =-α}pop(S-,α-){S--=--(s1,s2,...,s|Sk|-1)}---.
     {Sk|Sk| = α }(Sk, α) = pop(Sk){Sk = (sk1,sk2,...,sk|Sk|-1)}

This converts the pop operation into the pop operation introduced in Section 4.2, which allows reduction:

Reduction: Correct communication via push/pop to/from stack Sk is recognized and reduced via

    {}push(Sk, α){Sk = (sk1,sk2,...,skk,α )};{Sk k = α}(Sk, α) = pop(Sk){Sk = (sk1,sk2,...,skk )}
R1 :----------------------------|S-|------|S|------------------------------------|S-|--1--

This assures correct communication information received by the communication partner by pushing the same data α to the stack and fetching the same data α from the same stack. A reduction statement tests for such a correct communication and removes the statements, resulting in ϵ. We are allowed to do so, since the stack is kept in an unmodified state for all other edges accesses.

Commutativity: Commutative property for accessing different communication stacks

     {A}push(Sm,α){B-};{C}push(Sn⁄=m,β){D}-       {A}push(Sm,α){B-};{C}(Sn,β)=pop(Sn⁄=m){D}
R2 :  {C}push(Sn,β){D};{A }push(Sm,α){B} ,  R3 :  {C}(Sn,β):=pop(Sn){D};{A }push(Sm,β){B}
 R4  : {A}pop(Sm,α-){B};{C-}pop(Sn⁄=m-){D-},   R5 : {A}(Sn,α)=pop(Sn){B};{C}push(Sm-⁄=n,β){D}
        {C}pop(Sn,β){D};{A}pop(Sm ){B}            {C}push(Sm,β){D};{A}(Sn,α)=pop(Sn){B}
Those inference rules allow rearranging statements in case that they access different stacks. We emphasize here that this is only valid with constant data on each edge to be pushed to and fetched from stacks. This assumption would not be valid if e.g. data is fetched from one stack and data depending on this one pushed to another stack.

Joining consecutive communication data: In case of pushing or fetching edge data in the correct order with respect to the parent triangle allows to join data stored on the stack:

              k               k                      k              k
R7  : {A}push(S-,α{Ar,1}p)u{Bsh};({SCk,}αpru){shD(S}-,αr,2){D};,  R8 : {A}pop(S-,α{Ar,1)}p{oBp}(S;{kC,}αpro){pD(S},αr,2){D}; (4
Here, αr represents the edge data of the parent element. The edge data αr on the hypotenuse of the parent’s cell can be split into two edges creating edge data αr,1 and αr,2. This rule has to be proven to assure correct refinement operations.
Application of inference rules

We apply the rules R1-R8 to show the valid stack access for edge-based communication. Considering only new and old communication types, the proof is given without loss of generality by boundary edges assumed to not modify any communication stacks. For even traversals, the access order for the root triangle only considering the edge access (see Section 4.3.2) is given by

A (*,even),left := (e3,e2)    A(*,even),right := (e1) .                (4.19)
Distinguishing between K, V and H traversals is not required (see Theorem 4.3.2). We associate the edge information (a,b,c) to the edges (e1,e2,e3). Splitting a triangle using newest vertex bisection would then splits the communication information on the hypotenuse a by appending ,1 or ,2 to the subindex into (a,1,a,2). This would push two elements to the stack associated to e1 in the correct order. We assume the inserted edge information to be equal to an arbitrarily choosen d.

We map each new and old communication type of edge data α to push(Sk) and pop(Sk) to/from stack Sk. To avoid verification for all push/pop combinations, we use a generalization of stack operations

pp : ℂ → {push, pop}
for the parent edges only.

For the parent element of type even, this leads to the push and pop operations

pp(c )(Sleft,c);   pp(c )(Sleft,b);   pp(c )(Sright,a );.
    3                2                1
It has to be proven that by applying the stack operations for both children, the stack modifications are equal to only applying the stack communication patterns of the parent element.

Our communication scheme with type inheritance

childCfirst(c,even) → (c3,c1,n)    and     childCsecond(c,even) → (c2,o,c1)
can then be applied resulting directly in the code for the stack operations being executed:
                ∕∕ firstchild;
        {M  }   pp(c )(Sleft,c);   {N };
           1        3  right        1
        {M2 }  pp(c1)(Srigh,ta1);  {N2r};  r  r      r
           {}   push(S    ,d);   {S =  (s1,s2,...,s|Sr|,d)}

                ∕∕ secondchild;
        {M3 }   pp(c2)(Sleft,b);   {N3};
{Sr,Sr r = d}    pop(Sright,d);    {Sr = (sr,sr,...,srr   )}
     |S|               right             1  2      |S |-1
        {M4 }  pp(c1)(S    ,a2);  {N4};
Using commutative rules (R2-R5), we can exchange the stack operations to
        {M1 }   pp(c3)(S lef,tc);   {N1};
        {M3 }   pp(c2)(S   ,b);   {N3};

        {M2 }  pp(c1)(Sright,a1);  {N2};
           {}   push(Sright,d);   {Sr = (sr1,sr2,...,srr ,d)}
{Sr,Sr   = d}    pop(Sright,d);    {Sr = (sr,sr,...,s|Sr |  )}
     |Sr|               right             1  2      |Sr|-1
        {M4 }  pp(c1)(S    ,a2);  {N4};
and by applying the reduction rule, this yields the half-diamond operations
{M1 }   pp(c3)(S   ,c);   {N1 };
{M3 }   pp(c2)(Sleft,b);   {N3 };
                                                                     .    (4.20)
{M2 }  pp(c1)(Sright,a1);  {N2 };
{M4 }  pp(c1)(Sright,a2);  {N4 };
Further applying our reduction rule R7/8 completes the first part of the proof since the reduction is only achieved in case of an exchange of data in correct order and correct order of push operations. This leads to
{M1 }  pp (c3)(Sleft,c);  {N1};
{M3 }  pp (c2)(Sleft,b);  {N3};

{M2 }  pp(c1)(S    ,a);  {N4};
These stack operations on the data a, b and c are equal to the stack operations of the parent cell, assuming that this is the leaf cell. For odd element types, the verification is analogously given.

With our grids generated by the spacetree, we still have to prove the stack system for an entire grid. Without loss of generality, we only present this proof for diamond-shaped grid areas by applying coarsening rules, see Fig. 4.11.


Figure 4.11: Coarsening and refine operations with diamond shaped structure

We assemble two half-diamond operations (see Eqs. (4.20)) to operations of a full diamond and apply the coarsening operations. With operations on the right stack access represented by the symbol [X], this yields the following code

          {M1 }  pp(c3)(Sleft,b);  {N1 };
          {M2 }  pp(c2)(Sleft,c);  {N2 };

            { } push (Sright,a1); {Sr = (sr,sr,...,sr r,a1)};
                       right         r    1r  2r     |rS |
            { } push (S    ,a2); {S  = (s1,s2,...,s|Sr|,a2)};

                    ...[X ]...                                                .

{Sr, Srr =  a2}  pop(Sright,a2);  {Sr = (sr,sr,...,sr r  )};
   r  |Sr |             right         r    1r  2r     |rS |-1
{S  ,S|Sr| = a1}  pop(S    ,a1);  {S  = (s1,s2,...,s|Sr|-1)};

          {M7 }  pp(c3)(Sleft,d);  {N7 };
          {M8 }  pp(c2)(Sleft,e);  {N8 };
Applying the commutative and reduction rules, we can further reduce both push and pop operations to
{M1 }  pp(c3)(S lef,tb);  {N1};
{M2 }  pp(c2)(S   ,c);  {N2};

{M7 }  pp(c3)(Sleft,d);  {N7};
{M8 }  pp(c2)(Sleft,e);  {N8};
and with recursive induction, this results in a validated stack access. _

Theorem 4.7.2 (SFC stack communication order) We consider a traversal with stack-based communication and communicate the cell identifiers Ii via edges. Here, the identifiers Ii are increasing by traversing the cells following the SFC. Then it holds that at any time during the traversal all identifiers are ordered on the communication stack.

By communicating cell identifiers to adajcent cells, we follow the SFC. Then all push operations push identifiers of cells with the same or higher index. With the previous proof, we also assured the correct communication. _

We just introduced a method for validating the correct communication via the left- and right stacks for two-dimensional triangular grids. Such a way of validation can play an important role on the search for valid stack-communication properties for other SFC-induced grids such as hexagons or higher-dimensional shapes.