A program logic for obstruction-freedom

doi:10.1007/s11704-023-2774-9

Front. Comput. Sci.

2024, Vol. 18

Issue (6) : 186208 https://doi.org/10.1007/s11704-023-2774-9

RESEARCH ARTICLE

A program logic for obstruction-freedom

Zhao-Hui LI¹, Xin-Yu FENG^2,³(

)

¹. School of Computer Science and Technology, University of Science and Technology of China, Hefei 230026, China
². Department of Computer Science and Technology, Nanjing University, Nanjing 210023, China
³. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210023, China

Download: PDF(12601 KB) HTML
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

Abstract

Though obstruction-free progress property is weaker than other non-blocking properties including lock-freedom and wait-freedom, it has advantages that have led to the use of obstruction-free implementations for software transactional memory (STM) and in anonymous and fault-tolerant distributed computing. However, existing work can only verify obstruction-freedom of specific data structures (e.g., STM and list-based algorithms).

In this paper, to fill this gap, we propose a program logic that can formally verify obstruction-freedom of practical implementations, as well as verify linearizability, a safety property, at the same time. We also propose informal principles to extend a logic for verifying linearizability to verifying obstruction-freedom. With this approach, the existing proof for linearizability can be reused directly to construct the proof for both linearizability and obstruction-freedom.Finally, we have successfully applied our logic to verifying a practical obstruction-free double-ended queue implementation in the first classic paper that has proposed the definition of obstruction-freedom.

Keywords verification program logic progress properties obstruction-freedom concurrent objects

Corresponding Author(s): Xin-Yu FENG

Just Accepted Date: 12 July 2023 Issue Date: 08 October 2023

Cite this article:

Zhao-Hui LI,Xin-Yu FENG. A program logic for obstruction-freedom[J]. Front. Comput. Sci., 2024, 18(6): 186208.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-023-2774-9
https://academic.hep.com.cn/fcs/EN/Y2024/V18/I6/186208

Fig.1 Obstruction-free counter

Fig.2 Divergence caused by finite interference

Fig.3 Blocking Inc

Fig.4 Syntax of the programming language

Fig.5 States and event traces

Fig.6 Selected operational semantics rules. (a) Transitions made by the whole program; (b) transitions made by the individual thread; (c) transitions made by the client or the object method

Fig.7 Syntax of the assertion language

Fig.8 Semantics of assertions. (a) Semantics of relational state assertions P and Q; (b) semantics of relational rely/guarantee assertions R and G; (c) semantics of full assertions p and q

Fig.9 Inference rules

Fig.10 Auxiliary definitions

Fig.11 Structure of logic soundness proof

Fig.12 Overview of the deque

Fig.13 Transition caused by

rightPush

Fig.14 Abstract object

Fig.15 Auxiliary code for the implementation

Fig.16 Implementation of

rightPush

Fig.17

rightPush

with auxiliary code

Fig.18 Definitions of

I

and

P

Fig.19 Definition of

G r P u s h

and

R

Fig.20 Proof sketch

Fig.21 Proof sketch(sequential total correctness)

Fig.22 Auxiliary definitions for proof sketch

Fig.23 Implementation of

rightPop

1	L Lamport . Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, 1977, SE-3( 2): 125–143
2	M P, Herlihy J M Wing . Linearizability: a correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems, 1990, 12( 3): 463–492
3	M, Herlihy N Shavit . The Art of Multiprocessor Programming. Amsterdam: Morgan Kaufmann, 2008
4	H, Liang X Feng . Modular verification of linearizability with non-fixed linearization points. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2013, 459−470
5	Rocha Pinto P, da T, Dinsdale-Young P Gardner . TaDA: a logic for time and data abstraction. In: Proceedings of the 28th European Conference on Object-Oriented Programming. 2014, 207−231
6	R, Jung D, Swasey F, Sieczkowski K, Svendsen A, Turon L, Birkedal D Dreyer . Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. ACM SIGPLAN Notices, 2015, 50( 1): 637–650
7	Rocha Pinto P, da T, Dinsdale-Young P, Gardner J Sutherland . Modular termination verification for non-blocking concurrency. In: Proceedings of the 25th European Symposium on Programming. 2016, 176−201
8	Liang H, Feng X, Shao Z. Compositional verification of termination-preserving refinement of concurrent programs. In: Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 2014, 65
9	H, Liang X Feng . A program logic for concurrent objects under fair scheduling. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2016, 385−399
10	R, Guerraoui T A, Henzinger B, Jobstmann V Singh . Model checking transactional memories. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2008, 372−382
11	P, Abdulla S, Dwarkadas A, Rezine A, Shriraman Y Zhu . Verifying safety and liveness for the FlexTM hybrid transactional memory. In: Proceedings of 2013 Design, Automation & Test in Europe Conference & Exhibition. 2013, 785−790
12	A, Gotsman B, Cook M, Parkinson V Vafeiadis . Proving that non-blocking algorithms don’t block. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2009, 16−28
13	M Herlihy . Wait-free synchronization. ACM Transactions on Programming Languages and Systems, 1991, 13( 1): 124–149
14	Fraser K. Practical lock-freedom. No. UCAM-CL-TR-579. University of Cambridge, Computer Laboratory, 2004
15	M, Herlihy V, Luchangco M Moir . Obstruction-free synchronization: double-ended queues as an example. In: Proceedings of the 23rd International Conference on Distributed Computing Systems. 2003, 522−529
16	A, Saha A, Chatterjee N, Pal A, Ghosh N Chaki . A lightweight implementation of obstruction-free software transactional memory. In: Chaki R, Saeed K, Choudhury S, Chaki N, eds. Applied Computation and Security Systems. New Delhi: Springer, 2014, 67−84
17	A, Ghosh N Chaki . Design of a new OFTM algorithm towards abort-free execution. In: Proceedings of the 9th International Conference on Distributed Computing and Internet Technology. 2013, 255−266
18	Tabba F, Moir M, Goodman J R, Hay A W, Wang C. NZTM: nonblocking zero-indirection transactional memory. In: Proceedings of the 21st Annual Symposium on Parallelism in Algorithms and Architectures. 2009, 204−213
19	V J, Marathe III W N, Scherer M L Scott . Adaptive software transactional memory. In: Proceedings of the 19th International Symposium on Distributed Computing. 2005, 354−368
20	R, Guerraoui E Ruppert . Anonymous and fault-tolerant shared-memory computing. Distributed Computing, 2007, 20( 3): 165–177
21	Z, Bouzid M, Raynal P Sutra . Anonymous obstruction-free (n, k)-set agreement with n-k+1 atomic read/write registers. Distributed Computing, 2018, 31( 2): 99–117
22	K, Fraser T Harris . Concurrent programming without locks. ACM Transactions on Computer Systems, 2007, 25( 2): 5
23	M S, Moir V M, Luchangco M Herlihy . Obstruction-free data structures and mechanisms with separable and/or substitutable contention management mechanisms: US09052944B2. 2005–04-15
24	F E, Fich V, Luchangco M, Moir N Shavit . Obstruction-Free algorithms can be practically wait-free. In: Proceedings of the 19th International Conference on Distributed Computing. 2005, 78−92
25	H, Liang J, Hoffmann X, Feng Z Shao . Characterizing progress properties of concurrent objects via contextual refinements. In: Proceedings of the 24th International Conference on Concurrency Theory. 2013, 227−241
26	H, Liang X Feng . Progress of concurrent objects with partial methods. Proceedings of the ACM on Programming Languages, 2017, 2( POPL): 20
27	Z H, Li X Y Feng . Verifying contextual refinement with ownership transfer. Journal of Computer Science and Technology, 2021, 36( 6): 1342–1366
28	J, Hoffmann M, Marmar Z Shao . Quantitative reasoning for proving lock-freedom. In: Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science. 2013, 124−133
29	H, Liang X Feng . Progress of concurrent objects. Foundations and Trends® in Programming Languages, 2020, 5( 4): 282–414
30	I, Filipović P, O’Hearn N, Rinetzky H Yang . Abstraction for concurrent objects. Theoretical Computer Science, 2010, 411(51−52): 4379−4398

[1]	FCS-22774-OF-ZL_suppl_1	Download
[2]	FCS-22774-OF-ZL_suppl_2	Download

[1]	Shiwei LU, Ruihu LI, Wenbin LIU. FedDAA: a robust federated learning framework to protect privacy and defend against adversarial attack[J]. Front. Comput. Sci., 2024, 18(2): 182307-.
[2]	Shahbaz ALI, Hailong SUN, Yongwang ZHAO. Model learning: a survey of foundations, tools and applications[J]. Front. Comput. Sci., 2021, 15(5): 155210-.
[3]	Daian YUE, Vania JOLOBOFF, Frédéric MALLET. TRAP: trace runtime analysis of properties[J]. Front. Comput. Sci., 2020, 14(3): 143201-.
[4]	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.
[5]	Tun LI, Jun YE, Qingping TAN. Towards functional verifying a family of SystemC TLMs[J]. Front. Comput. Sci., 2020, 14(1): 53-66.
[6]	Abdelkrim CHEBIEB, Yamine AIT AMEUR. A formal model for plastic human computer interfaces[J]. Front. Comput. Sci., 2018, 12(2): 351-375.
[7]	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.
[8]	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.
[9]	Jiankun HE,Xishun ZHAO. Reasoning about actions with loops via Hoare logic[J]. Front. Comput. Sci., 2016, 10(5): 870-888.
[10]	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.
[11]	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.
[12]	Fei HE,Xiaoyu SONG,Ming GU,Jiaguang SUN. Generalized interface automata with multicast synchronization[J]. Front. Comput. Sci., 2015, 9(1): 1-14.
[13]	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.
[14]	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.
[15]	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.

Viewed

Full text

Abstract

Cited

Shared

Discussed