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
(6)
Mutual Exclusion
Proof Assistant
Proof of Correctness
Satisfiability
Temporal Logic
First Come First Serve
Subscribe
Academic
Publications
Nonatomic dual bakery algorithm with bounded tokens
Nonatomic dual bakery algorithm with bounded tokens,10.1007/s0023601101320,Acta Informatica,Alex A. Aravind,Wim H. Hesselink
Edit
Nonatomic dual bakery algorithm with bounded tokens
BibTex

RIS

RefWorks
Download
Alex A. Aravind
,
Wim H. Hesselink
A simple
mutual exclusion
algorithm is presented that only uses nonatomic shared variables of bounded size, and that satisfies bounded overtaking. When the shared variables behave atomically, it has the firstcomefirstserved property (FCFS). Nonatomic access makes information vulnerable. The effects of this can be mitigated by minimizing the information and by spreading it over more variables. The design approach adopted here begins with such mitigating efforts. These resulted in an algorithm with a proof of correctness, first for atomic variables. This proof is then used as a blueprint for the simultaneous development of the algorithm for nonatomic variables and its proof.
Mutual exclusion
is proved by means of invariants. Bounded overtaking and liveness under weak fairness are proved with invariants and variant functions. Liveness under weak fairness is formalized and proved in a settheoretic version of temporal logic. All these assertions are verified with the
proof assistant
PVS. We heavily rely on the possibility offered by a
proof assistant
like PVS to reuse proofs developed for one context in a different context.
Journal:
Acta Informatica  ACTA
, vol. 48, no. 2, pp. 6796, 2011
DOI:
10.1007/s0023601101320
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.
(
www.springerlink.com
)
(
www.springerlink.com
)
(
www.informatik.unitrier.de
)
(
dx.doi.org
)
More »
References
(39)
The Existence of Refinement Mappings
(
Citations: 485
)
Martín Abadi
,
Leslie Lamport
Conference:
Logic in Computer Science  LICS
, pp. 165175, 1988
Sharedmemory Mutual Exclusion: Major Research Trends Since 1986
(
Citations: 36
)
James H. Anderson
,
Yongjik Kim
Journal:
Distributed Computing  DC
, 2001
An arbitration algorithm for multiport memory systems
(
Citations: 1
)
Alex A. Aravind
Journal:
Ieice Electronic Express
, vol. 2, no. 19, pp. 488494, 2005
A queue based mutual exclusion algorithm
(
Citations: 4
)
Alex A. Aravind
,
Wim H. Hesselink
Journal:
Acta Informatica  ACTA
, vol. 46, no. 1, pp. 7386, 2009
Solution of a problem in concurrent programming control
(
Citations: 459
)
Edsger W. Dijkstra
Journal:
Communications of The ACM  CACM
, vol. 8, no. 9, 1965