Please wait a minute...
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Front. Comput. Sci.    2014, Vol. 8 Issue (6) : 958-976    https://doi.org/10.1007/s11704-014-3342-0
RESEARCH ARTICLE
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
 Download: PDF(1038 KB)  
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
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
 Cite this article:   
Xiaoxiao YANG,Yu ZHANG,Ming FU, et al. A temporal programming model with atomic blocks based on projection temporal logic[J]. Front. Comput. Sci., 2014, 8(6): 958-976.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-014-3342-0
https://academic.hep.com.cn/fcs/EN/Y2014/V8/I6/958
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
[1] Daian YUE, Vania JOLOBOFF, Frédéric MALLET. TRAP: trace runtime analysis of properties[J]. Front. Comput. Sci., 2020, 14(3): 143201-.
[2] Yuanrui ZHANG, Frédéric MALLET, Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.
[3] Tun LI, Jun YE, Qingping TAN. Towards functional verifying a family of SystemC TLMs[J]. Front. Comput. Sci., 2020, 14(1): 53-66.
[4] Ying JIANG, Shichao LIU, Thomas EHRHARD. A fully abstract semantics for value-passing CCS for trees[J]. Front. Comput. Sci., 2019, 13(4): 828-849.
[5] Thierry GAUTIER, Clément GUY, Alexandre HONORAT, Paul LE GUERNIC, Jean-Pierre TALPIN, Loïc BESNARD. Polychronous automata and their use for formal validation of AADL models[J]. Front. Comput. Sci., 2019, 13(4): 677-697.
[6] Abdelkrim CHEBIEB, Yamine AIT AMEUR. A formal model for plastic human computer interfaces[J]. Front. Comput. Sci., 2018, 12(2): 351-375.
[7] Xiaobing WANG, Cong TIAN, Zhenhua DUAN, Liang ZHAO. MSVL: a typed language for temporal logic programming[J]. Front. Comput. Sci., 2017, 11(5): 762-785.
[8] Yongwang ZHAO, Zhibin YANG, Dianfu MA. A survey on formal specification and verification of separation kernels[J]. Front. Comput. Sci., 2017, 11(4): 585-607.
[9] Ruifeng XU,Lin GUI,Qin LU,Shuai WANG,Jian XU. Incorporating multi-kernel function and Internet verification for Chinese person name disambiguation[J]. Front. Comput. Sci., 2016, 10(6): 1026-1038.
[10] Jiankun HE,Xishun ZHAO. Reasoning about actions with loops via Hoare logic[J]. Front. Comput. Sci., 2016, 10(5): 870-888.
[11] Xiao PAN,Weizhang CHEN,Lei WU,Chunhui PIAO,Zhaojun HU. Protecting personalized privacy against sensitivity homogeneity attacks over road networks in mobile services[J]. Front. Comput. Sci., 2016, 10(2): 370-386.
[12] Yang ZHANG,Xinyu FENG. An operational happens-before memory model[J]. Front. Comput. Sci., 2016, 10(1): 54-81.
[13] Yu ZHOU,Yankai HUANG,Ou WEI,Zhiqiu HUANG. Verifying specifications with associated attributes in graph transformation systems[J]. Front. Comput. Sci., 2015, 9(3): 364-374.
[14] Yanhong HUANG,Jifeng HE,Huibiao ZHU,Yongxin ZHAO,Jianqi SHI,Shengchao QIN. Semantic theories of programs with nested interrupts[J]. Front. Comput. Sci., 2015, 9(3): 331-345.
[15] Xuzhou LI,Yilong YIN,Yanbin NING,Gongping YANG,Lei PAN. A hybrid biometric identification framework for high security applications[J]. Front. Comput. Sci., 2015, 9(3): 392-401.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed