Please wait a minute...
Shopping Cart Email List Chinese
Advanced Search Fig/Tab
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

Featured Articles  |  Most Downloaded  |  Most Reading
Online Submission Subscribe to Our RSS Content Feed
Front. Comput. Sci.    2010, Vol. 4 Issue (1) : 65-77    https://doi.org/10.1007/s11704-009-0067-6
Research articles
Formal verification of concurrent programs with read-write locks
Ming FU,Yu ZHANG,Yong LI,
School of Computer Science and Technology, University of Science and Technology of China, Hefei 230027, China；Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou 215123, China;
 Download: PDF(415 KB)  
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
Abstract Read-write locking is an important mechanism to improve concurrent granularity, but it is difficult to reason about the safety of concurrent programs with read-write locks. Concurrent separation logic (CSL) provides a simple but powerful technique for locally reasoning about concurrent programs with mutual exclusive locks. Unfortunately, CSL cannot be directly applied to reasoning about concurrent programs with read-write locks due to the different concurrent control mechanisms.
This paper focuses on extending CSL and presenting a proof-carrying code (PCC) system for reasoning about concurrent programs with read-write locks. We extend the heap model with a writing permission set, denoted as logical heap, then define “strong separation” and “weak separation” over logical heap. Following CSL’s local-reasoning idea, we develop a novel program logic to enforce weak separations of heap between different threads and provide verification of concurrent programs with read-write locks.
Keywords verification      concurrent separation logic      mutual exclusive locks      read-write locks      
Issue Date: 05 March 2010
 Cite this article:   
Ming FU,Yong LI,Yu ZHANG. Formal verification of concurrent programs with read-write locks[J]. Front. Comput. Sci., 2010, 4(1): 65-77.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-009-0067-6
https://academic.hep.com.cn/fcs/EN/Y2010/V4/I1/65
Hearn O P W. Resources, concurrency, and local reasoning. Theoretical Computer Science, 2007, 375(1―3): 271―307
Hoare C A R. Towards a theory of parallel programming. In: Hoare C A R and Perrott R H, eds. Operating Systems Techniques. Academic Press, 1972, 61―71
The Coq Development Team. The Coq proof assistant reference manual. The Coq release v8.0, October2004
Necula G.Proof-carryingcode. In: Proceedings of the 24th ACM SIGPLAN-SIGACTSymposium on Principles of Programming Languges. ACM Press, January1997, 106―119
Reynolds J C. Separation logic: A logic for shared mutable data structures. In: Proceedings of the 17th IEEE Symposium on Logicin Computer Science, July2002, 55―74
Yu D C, Shao Z. Verification of safety propertiesfor concurrent assembly code. In: Proceedingsof the 9th ACM SIGPLAN International Conference on Functional Programming, September2004, 19―21
Hearn O PW. Resources, concurrency and local reasoning. In: Proceedings of the 15th International Conference on Concurrency Theory, 2004, LNCS, 3170: 49―67
Wright A K, Felleisen M. A syntactic approach to typesoundness. Information and Computation, 1994, 115(1): 38―94

doi: 10.1006/inco.1994.1093
The Coq Development Team. The Coq proof assistant reference manual. The Coq release v7.1, October2001
Owicki S, Gries D. Verifying properties of parallelprograms: an axiomatic approach. Communicationsof the ACM, 1976, 19(5): 279―285

doi: 10.1145/360051.360224
Jones C B. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 1983, 5(4): 596―619

doi: 10.1145/69575.69577
Feng X, Shao Z. Modular verification of concurrentassembly code with dynamic thread creation and termination. In: Proceedings of the 10th ACM SIGPLAN internationalconference on Functional programming, 2005, 26―28
Feng X, Ferreira R, Shao Z. On the relationship between concurrent separation logicand assume-guarantee reasoning. In: Proceedingsof the 16th European Symposium on Programming, 2007, 173―188
Brookes S. Asemantics for concurrent separation logic. Theoretical Computer Science, 2007, 375: 227―270

doi: 10.1016/j.tcs.2006.12.034
Ishtiaq S S, Hearn O P W. BI as an assertion languagefor mutable data structures. In: Proceedingsof the 28th ACM SIGPLAN-SIGACT symposium on Principles of ProgrammingLanguages, 2001, 14―26
Vafeiadis V, Parkinson M J. A marriage of rely/guaranteeand separation logic. In: Proceedings ofthe 18th International Conference on Concurrency Theory, 2007, 256―271
Bornat R, Calcagno C, Hearn O PW, et al. Permission accounting in separation logic. In: Proceedings of the 32nd ACM SIGPLAN-SIGACTSymposium on Principles of Programming Languages, 2005, 259―270
[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] Abdelkrim CHEBIEB, Yamine AIT AMEUR. A formal model for plastic human computer interfaces[J]. Front. Comput. Sci., 2018, 12(2): 351-375.
[5] 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.
[6] 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.
[7] Jiankun HE,Xishun ZHAO. Reasoning about actions with loops via Hoare logic[J]. Front. Comput. Sci., 2016, 10(5): 870-888.
[8] 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.
[9] 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.
[10] Fei HE,Xiaoyu SONG,Ming GU,Jiaguang SUN. Generalized interface automata with multicast synchronization[J]. Front. Comput. Sci., 2015, 9(1): 1-14.
[11] Xiaoxiao YANG,Yu ZHANG,Ming FU,Xinyu FENG. A temporal programming model with atomic blocks based on projection temporal logic[J]. Front. Comput. Sci., 2014, 8(6): 958-976.
[12] Yuanjie SI, Jun SUN, Yang LIU, Jin Song DONG, Jun PANG, Shao Jie ZHANG, Xiaohu YANG. Model checking with fairness assumptions using PAT[J]. Front. Comput. Sci., 2014, 8(1): 1-16.
[13] Jean-Vivien MILLO, Frédéric MALLET, Anthony COADOU, S RAMESH. Scenario-based verification in presence of variability using a synchronous approach[J]. Front Comput Sci, 2013, 7(5): 650-672.
[14] Van Chan NGO, Jean-Pierre TALPIN, Thierry GAUTIER, Paul Le GUERNIC, Lo?c BESNARD. Formal verification of synchronous data-flow program transformations toward certified compilers[J]. Front Comput Sci, 2013, 7(5): 598-616.
[15] Zhiyuan LIU, Jun PANG, Chenyi ZHANG. Design and formal verification of a CEM protocol with transparent TTP[J]. Front Comput Sci, 2013, 7(2): 279-297.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed