|
|
A temporal programming model with atomic blocks based on projection temporal logic |
Xiaoxiao YANG1,*( ),Yu ZHANG1,Ming FU2,Xinyu FENG2 |
1. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China 2. Suzhou Institute for Advanced Study University of Science & Technology of China, SuZhou 215123, China |
|
|
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
semantics
temporal logic programming
verification
framing
atomic blocks
|
Corresponding Author(s):
Xiaoxiao YANG
|
Issue Date: 27 November 2014
|
|
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 18th 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
https://doi.org/10.1016/S0747-7171(89)80070-7
|
8 |
Lamport L. The temporal logic of actions. ACM Transactions on Programming Languages Systems, 1994, 16(3): 872-923
https://doi.org/10.1145/177492.177726
|
9 |
Rondogiannis P, Gergatsoulis M, Panayiotopoulos T. Branching-time logic programming: the language cactus and its applications. Computer Language, 1998, 24(3): 155-178
https://doi.org/10.1016/S0096-0551(98)00009-5
|
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
https://doi.org/10.1007/BF02944904
|
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
https://doi.org/10.1016/j.jlap.2008.08.001
|
15 |
Zhang N, Duan Z, Tian C. A cylinder computation model for manycore parallel computing. Theoretical Computer Science, 2013, 497: 68-83
https://doi.org/10.1016/j.tcs.2012.02.011
|
16 |
Tian C, Duan Z. Complexity of propositional projection temporal logic with Star. Mathematical Structures in Computer Science, 2009, 19(1): 73-100
https://doi.org/10.1017/S096012950800738X
|
17 |
Bidoit. N. Negation in rule-based data base languages: a survey. Theoretical Computer Science, 1991, 78(1): 3-83
https://doi.org/10.1016/0304-3975(51)90003-5
|
18 |
Duan Z, Tian C, Zhang L. A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica, 2008, 45: 43-78
https://doi.org/10.1007/s00236-007-0062-z
|
19 |
Duan Z, Zhang N, Koutny M. A complete proof system for propositional projection temporal logic. Theoretical Computer Science, 2013, 497: 84-107
https://doi.org/10.1016/j.tcs.2012.01.026
|
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
https://doi.org/10.1007/BF01211458
|
25 |
Best E, Randell B. A formal model of atomicity in asyn chronous systems. Acta Informatica, 1981, 16: 93-124
https://doi.org/10.1007/BF00289593
|
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
https://doi.org/10.1006/jpdc.1998.1446
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
|
Shared |
|
|
|
|
|
Discussed |
|
|
|
|