2006
Reasoning about data-parallel pointer programs in a modal extension of separation logic
ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS
- Volume
- 4019
- Number
- First page
- 293
- Last page
- 307
- Language
- English
- Publishing type
- Research paper (scientific journal)
- Publisher
- SPRINGER-VERLAG BERLIN
This paper proposes a modal extension of Separation Logic [1, 2] 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.
- Link information
- ID information
-
- ISSN : 0302-9743
- Web of Science ID : WOS:000239425400023