Verifying visibility-based weak consistency

DOI10.1007/978-3-030-44914-8_11MaRDI QIDQ5041095zbMATH OpenOpenAlexFDO

Authors Siddharth Krishna, Michael Emmi, Constantin Enea, Dejan Jovanović

Publication date 13 October 2022

Published in Programming Languages and Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1911.01508

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Monitoring weak consistency
• Verifying concurrent programs against sequential specifications
• scientific article; zbMATH DE number 1979557
• Linearizability on hardware weak memory models
• Testing and verifying concurrent objects

Cites work

• \textsc{Poling}: SMT aided linearizability proofs
• An integrated specification and verification technique for highly concurrent data structures
• Aspect-oriented linearizability proofs
• Automated Deduction – CADE-20
• Automated verification of practical garbage collectors
• Comparison Under Abstraction for Verifying Linearizability
• CONCUR 2004 - Concurrency Theory
• Dafny: an automatic program verifier for functional correctness
• E-matching for fun and profit
• Forward and backward simulations. I. Untimed Systems
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Local linearizability for concurrent container-type data structures
• On abstraction and compositionality for weak-memory linearisability
• Owicki-Gries reasoning for weak memory models
• Proving linearizability using forward simulations
• Proving linearizability using partial orders
• Quantitative relaxation of concurrent data structures
• Replicated data types, specification, verification, optimality
• RGSep Action Inference
• Shape-Value Abstraction for Verifying Linearizability
• The existence of refinement mappings
• Verifying properties of parallel programs

Cited in

(3)

• Checking robustness between weak transactional consistency models
• Y-invalidate: A new protocol for implementing weak consistency in DSM systems
• Monitoring weak consistency

Describes a project that uses

Uses Software

• Dafny
• GRASShopper

This page was built for publication: Verifying visibility-based weak consistency

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5041095)