Reasoning About Data-Parallel Pointer Programs in a Modal Extension of Separation Logic

This paper proposes a modal extension of Separation Logic [8, 11] for reasoning about data-parallel programs that manipulate heap allocated linked data structures. Separation Logic provides a formal means for expressing allocation of disjoint substructures, which are to be processed in parallel. A modal operator is also introduced to relate the global property of a parallel operation with the local property of each sequential execution running in parallel. The effectiveness of the logic is demonstrated through a formal reasoning on the parallel list scan algorithm featuring the pointer jumping technique.

• Type: Conference
• Year: 2006
• Where: AMAST
• Authors: Susumu Nishimura
• Keywords: AMAST 2006, Modal Extension, Parallel List Scan, Separation Logic, Software Engineering