Matthew Parkinson
ABSTRACT
This paper contributes to the development of techniques for the modular proof of programs that include concurrent algorithms. We present a proof of a non-blocking concurrent algorithm, which provides a shared stack. The inter-thread interference, which is essential to the algorithm, is confined in the proof and the specification to the modular operations, which perform push and pop on the stack. This is achieved by the mechanisms of separation logic. The effect is that inter-thread interference does not pollute specification or verification of clients of the stack.
- R. Bornat, C. Calcagno, P. W. O'Hearn, and M. J. Parkinson. Permission accounting in separation logic. In Proceedings of popl, pages 259--270, 2005. Google Scholar
Digital Library
- R. Bornat, C. Calcagno, and H. Yang. Variables as resource in separation logic. In Proceedings of MFPS XXI. Elsevier ENTCS, May 2005.Google Scholar
- P. Brinch Hansen, editor. The Origin of Concurrent Programming. Springer-Verlag, 2002. Google ScholarDigital Library
- S. Brookes. A semantics for concurrent separation logic. Invited paper, in Proceedings of CONCUR, 2004.Google Scholar
- E. W. Dijkstra. Cooperating sequential processes. In F. Genuys, editor, Programming Languages, pages 43--112. Academic Press, 1968. Reprinted in {3}.Google Scholar
- T. Harris, S. Marlow, S. Peyton-Jones, and M. P. Herlihy. Composable memory transactions. In Proceedings of PPOPP, 2005. Google ScholarDigital Library
- M. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463--492, 1990. Google ScholarDigital Library
- M. P. Herlihy and J. E. B. Moss. Transactional memory: architectural support for lock-free data structures. In ISCA '93: Proceedings of the 20th annual international symposium on Computer architecture, pages 289--300, 1993. Google ScholarDigital Library
- C. B. Jones. Specification and design of (parallel) programs. In IFIP Congress, pages 321--332, 1983.Google Scholar
- M. M. Michael. Hazard pointers: Safe memory reclamation for lock-free objects. IEEE Trans. Parallel Distrib. Syst., 15(6):491--504, 2004. Google ScholarDigital Library
- P. W. O'Hearn. Resources, concurrency and local reasoning. To appear in Theoretical Computer Science; preliminary version in CONCUR'04. Google ScholarDigital Library
- V. Vafeiadis, M. Herlihy, T. Hoare, and M. Shapiro. Proving correctness of highly-concurrent linearisable objects. In Proceedings of PPoPP, pages 129--136, 2006. Google ScholarDigital Library
Index Terms
- Modular verification of a non-blocking stack
Recommendations
Modular verification of a non-blocking stack
Proceedings of the 2007 POPL ConferenceThis paper contributes to the development of techniques for the modular proof of programs that include concurrent algorithms. We present a proof of a non-blocking concurrent algorithm, which provides a shared stack. The inter-thread interference, which ...
Grasping the gap between blocking and non-blocking transactional memories
Transactional memory (TM) is an inherently optimistic abstraction: it allows concurrent processes to execute sequences of shared-data accesses (transactions) speculatively, with an option of aborting them in the future. Early TM designs avoided using ...
Mechanized verification of fine-grained concurrent programs
PLDI '15Efficient concurrent programs and data structures rarely employ coarse-grained synchronization mechanisms (i.e., locks); instead, they implement custom synchronization patterns via fine-grained primitives, such as compare-and-swap. Due to sophisticated ...
Comments