A temporal programming model with atomic blocks based on projection temporal logic

Abstract

Atomic blocks, a high-level language construct that allows programmers to explicitly specify the atomicity of operations without worrying about the implementations, are a promising approach that simplifies concurrent programming. On the other hand, temporal logic is a successful model in logic programming and concurrency verification, but none of existing temporal programming models supports concurrent programming with atomic blocks yet. In this paper, we propose a temporal programming model (αPTL) which extends the projection temporal logic (PTL) to support concurrent programming with atomic blocks. The novel construct that formulates atomic execution of code blocks, which we call atomic interval formulas, is always interpreted over two consecutive states, with the internal states of the block being abstracted away. We show that the framing mechanism in projection temporal logic also works in the new model, which consequently supports our development of an executive language. The language supports concurrency by introducing a loose interleaving semantics which tracks only the mutual exclusion between atomic blocks. We demonstrate the usage of αPTL by modeling and verifying both the fine-grained and coarse-grained concurrency.

Keywords

atomic blocks / semantics / temporal logic programming / verification / framing

References

[1] Herlihy M, Shavit N. The Art of Multiprocessor Programming. Elsevier, 2009

[2] Vafeiadis V, Parkinson M J A. Marriage of rely/guarantee and separation logic. In: Proceedings of the 18th International Conference on Concurrency Theory. 2007, 4703: 256-271

[3] Zyulkyarov F, Harris T, Unsal O S, Cristal A, Valeroh M. Debugging programs that use atomic blocks and transactional memory. In: Proceedings of the 15th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. 2010, 57-66

[4] Harris T, Fraser K. Language support for lightweight transactions. In: Proceedings of the 18th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications. 2003, 388-402

[5] Ni Y, Welc A, Adl-Tabatabai A, Bach M, Berkowits S, Cownie J, Geva R, Kozhukow S, Narayanaswamy R. Design and implementation of transactional constructs for C/C⁺⁺. In: Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications. 2008, 195-212

[6] Pnueli A. The temporal logic of programs. In: Proceedings of the 18^th IEEE Annual Symposium on Foundations of Computer Science. 1977, 46-57

[7] Abadi M, Manna Z. Temporal logic programming. Journal of Symbolic Computation, 1989, 8(1-3): 277-295

[8] Lamport L. The temporal logic of actions. ACM Transactions on Programming Languages Systems, 1994, 16(3): 872-923

[9] Rondogiannis P, Gergatsoulis M, Panayiotopoulos T. Branching-time logic programming: the language cactus and its applications. Computer Language, 1998, 24(3): 155-178

[10] Moszkowski B C. Executing Temporal Logic Programs. Cambridge University Press, 1986

[11] Duan Z, Yang X, Koutny M. Semantics of framed temporal logic programs. In: Proceedings of the 21st International Conference on Logic Programming. 2005, 3668: 356-370

[12] Duan Z, Koutny M. A framed temporal logic programming language. Journal of Computer Science and Technology, 2004, 19(1): 341-351

[13] Yang X, Zhang Y, Fu M, Feng X. A concurrent temporal programming model with atomic blocks. In: Proceedings of the 14th International Conference on Formal Engineering Methods. 2012, 7635: 22-37

[14] Yang X, Duan Z. Operational semantics of framed tempura. Journal of Logic and Algebraic Programming, 2008, 78(1): 22-51

[15] Zhang N, Duan Z, Tian C. A cylinder computation model for manycore parallel computing. Theoretical Computer Science, 2013, 497: 68-83

[16] Tian C, Duan Z. Complexity of propositional projection temporal logic with Star. Mathematical Structures in Computer Science, 2009, 19(1): 73-100

[17] Bidoit. N. Negation in rule-based data base languages: a survey. Theoretical Computer Science, 1991, 78(1): 3-83

[18] Duan Z, Tian C, Zhang L. A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica, 2008, 45: 43-78

[19] Duan Z, Zhang N, Koutny M. A complete proof system for propositional projection temporal logic. Theoretical Computer Science, 2013, 497: 84-107

[20] Vafeiadis V. Modular Fine-Grained Concurrency Verification. Cambridge University, 2008

[21] Tang C S. A temporal logic language oriented toward software engineering — introduction to XYZ system (I). Chinese Journal of Advanced Software Research, 1994, 1: 1-27

[22] Schellhorn G, Tofan B, Ernst G, Reif W. Interleaved programs and rely-guarantee reasoning with ITL. In: Proceedings of 18th International Symposium on Temporal Representation and Reasoning. 2011, 99-106

[23] Derrick J, Schellhorn G, Wehrheim H. Verifying linearisability with potential linearisation points. In: Proceedings of the 17th International Symposium on Formal Methods, 2011, 6664, 327-337

[24] Knijnenburg P, Kok J. The semantics of the combination of atomized statements and parallel choice. Formal Aspects of Computing, 1997, 9: 518-536

[25] Best E, Randell B. A formal model of atomicity in asyn chronous systems. Acta Informatica, 1981, 16: 93-124

[26] Michael M M, Scott M L. Nonblocking algorithms and preemptionsafe locking on multiprogrammed shared memory multiprocessors. Journal of Parallel and Distributed Computing, 1998, 51(1): 1-26

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag Berlin Heidelberg