Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(2)
Theorem Prover
Theorem Proving
Subscribe
Academic
Publications
Mechanically verified proof obligations for linearizability
Mechanically verified proof obligations for linearizability,10.1145/1889997.1890001,ACM Transactions on Programming Languages and Systems,John Derrick
Edit
Mechanically verified proof obligations for linearizability
(
Citations: 2
)
BibTex

RIS

RefWorks
Download
John Derrick
,
Gerhard Schellhorn
,
Heike Wehrheim
Concurrent objects are inherently complex to verify. In the late 80s and early 90s, Herlihy and Wing proposed linearizability as a correctness condition for concurrent objects, which, once proven, allows us to reason about concurrent objects using pre and postconditions only. A concurrent object is linearizable if all of its operations appear to take effect instantaneously some time between their invocation and return. In this article we define simulationbased proof conditions for linearizability and apply them to two concurrent implementations, a lockfree stack and a set with lockcoupling. Similar to other approaches, we employ a
theorem prover
(here, KIV) to mechanize our proofs. Contrary to other approaches, we also use the prover to mechanically check that our proof obligations actually guarantee linearizability. This check employs the original ideas of Herlihy and Wing of verifying linearizability via possibilities.
Journal:
ACM Transactions on Programming Languages and Systems  TOPLAS
, vol. 33, no. 1, pp. 143, 2011
DOI:
10.1145/1889997.1890001
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
portal.acm.org
)
(
portal.acm.org
)
(
www.informatik.unitrier.de
)
(
doi.acm.org
)
More »
Citation Context
(2)
...To verify linearizability [11] and [
13
] give modular proof obligations, that reduce the problem to two processes by exploiting their symmetry...
Gerhard Schellhorn
,
et al.
Formal Verification of LockFree Algorithms
...The technique extends our previous approach [4,
5
] to cope with the class of algorithms like the lazy set...
...1 Line R2b is the only modification of remove compared to the pessimistic version studied in [
5
]...
...These operations are then promoted (using the same standard schema as in [
5
]) to operations COp j on CS for each process p ∈ P , which work on the local state lsf (p)...
...Our proof technique introduced in [4] and further elaborated in [
5
] relies on a proof of linearisability via refinement...
...For some simpler classes of algorithms (e.g., stack and nonlazy set considered in [
5
]), LPs can be determined from the current state of a process (basically, its program counter), and in our methodology are fixed by defining a socalled status function assigning values from a type STATUS :...
...With the help of the status function we define specific statusdependent proof obligations in [4,
5
]...
...The proof obligations in [
5
] are particular instances of forward simulations...
...For our case study, the proof obligations of [
5
] are sufficient to verify the add and remove operation, where the LP can be identified in the code...
...Defining the invariants: As in [
5
], in addition to the abstraction function our theory requires a local invariant INV on GS × LS to capture constraints which are always valid in our linked list implementation (e.g., that tail is always reachable from head)...
...The latter point requires an extension to the theory developed in [
5
]...
...Many of these instances are similar to the ones for verifying the pessimistic algorithm in [
5
]...
...With these instances the verification of the proof obligation (LPO) in KIV is now only slightly more difficult than for the pessimistic case, and the additional complexity is solely due to the more complex invariant NODEINV . The technical encoding of Z schemata in KIV is the same as described in Section 7 of [
5
]...
John Derrick
,
et al.
Verifying Linearisability with Potential Linearisation Points
References
(45)
Formal Construction of a Nonblocking Concurrent Queue Algorithm (a Case Study in Atomicity)
(
Citations: 15
)
Jeanraymond Abrial
,
Dominique Cansell
Journal:
Journal of Universal Computer Science  J.UCS
, vol. 11, no. 5, pp. 744770, 2005
Comparison Under Abstraction for Verifying Linearizability
(
Citations: 31
)
Daphna Amit
,
Noam Rinetzky
,
Thomas W. Reps
,
Mooly Sagiv
,
Eran Yahav
Conference:
Computer Aided Verification  CAV
, pp. 477490, 2007
The Spec# Programming System: An Overview
(
Citations: 478
)
Mike Barnett
,
Rustan Leino
,
Wolfram Schulte
Conference:
Construction and Analysis of Safe, Secure, and Interoperable Smart Devices  CASSIS
, 2004
Proving Linearizability with Temporal Logic
(
Citations: 4
)
S. Baumler
,
M. Balser
,
W. Reif
,
G. Schellhorn
Published in 2008.
Concurrency of Operations on BTrees
(
Citations: 217
)
Rudolf Bayer
,
Mario Schkolnick
Journal:
Acta Informatica  ACTA
, vol. 9, pp. 121, 1977
Sort by:
Citations
(2)
Formal Verification of LockFree Algorithms
Gerhard Schellhorn
,
Simon Bäumler
Conference:
Int. Conf. on Application of Concurrency to System Design  ACSD
, pp. 1318, 2009
Verifying Linearisability with Potential Linearisation Points
(
Citations: 1
)
John Derrick
,
Gerhard Schellhorn
,
Heike Wehrheim