Formalizing determinacy of concurrent revisions

descriptionPublicationkeyboard_double_arrow_right Article , Preprint , Conference object 20 Jan 2020Embargo end date: 01 Dec 2019 Netherlands Publisher:ACMJournal:Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and ProofsFunded by:NWO | ECiDA: Evolutionary chang...

Authors: Roy Overbeek;

doi: 10.1145/3372885.3373820 , 10.48550/arxiv.1912.09741

arXiv: 1912.09741

handle: 1871.1/fbeb927a-aa9e-4ee2-a437-132928c642f3

Formalizing determinacy of concurrent revisions

- Summary
- Subjects
- Metrics

Abstract

Concurrent revisions is a concurrency control model designed to guarantee determinacy, meaning that the outcomes of programs are uniquely determined. This paper describes an Isabelle/HOL formalization of the model's operational semantics and proof of determinacy. We discuss and resolve subtle ambiguities in the operational semantics and simplify the proof of determinacy. Although our findings do not appear to correspond to bugs in implementations, the formalization highlights some of the challenges involved in the design and verification of concurrency control models.

To appear in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '20), January 20--21, 2020, New Orleans, LA, USA. ACM, New York, NY, USA

Country

Netherlands

Related Organizations

Computer Science, Theoretical Computer Science
Netherlands
VU Research Institutes, Network Institute
Netherlands
Vrije Universiteit Amsterdam
Netherlands
Research Programmes - Computer Science, Theoretical Computer Science - research programme
Netherlands

Keywords

FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Concurrency control models, Proof assistants, Isabelle/HOL, Logic in Computer Science (cs.LO)

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	0
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average