Concurrency analysis of the 2D longest-edge refinement algorithm using trace theory

This paper applies trace theory to Rivara’s longest-edge refinement algorithm. This derivation aims to obtain formal verification of a parallel implementation of the longest-edge algorithm. Rivara’s longest-edge refinement can be used for Adaptive Mesh Refinement, a very important technique to reduce the computational times of Finite Element simulations. A correct and efficient implementation of the Rivara algorithm, as proposed in this paper, will ease the adoption of parallel adaptive mesh refinement algorithms. The mesh representation has been developed especially for concurrency analysis. We have defined all the atomic operations that need to be performed to obtain a refined conformal mesh. We have specified the dependencies between these operations and the flow diagram of the operations to obtain the trace, which is defined in pseudocode. Finally, we have derived the Diekert graph and its associated Foata Normal Form for two examples of mesh refinement, one with only one triangle to be refined and the other with two triangles. The results provide a trace-theory basis for verified scheduling of concurrent longest-edge refinement on shared-memory CPU architectures.