Parallelized sequential composition and hardware weak memory models

DOI10.1007/978-3-030-92124-8_12zbMath1522.68147OpenAlexW4205329012MaRDI QIDQ6045051

Robert J. Colvin

Publication date: 26 May 2023

Published in: Software Engineering and Formal Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-92124-8_12

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Reasoning about promises in weak memory models with event structures ⋮ A fine-grained semantics for arrays and pointers under weak memory models

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A semantics for concurrent separation logic
• A calculus of communicating systems
• An axiomatic proof technique for parallel programs
• Maude: specification and programming in rewriting logic
• A structural approach to operational semantics
• A wide-spectrum language for verification of programs on weak memory models
• A denotational semantics for SPARC TSO
• Explaining relaxed memory models with program transformations
• A Calculus for Relaxed Memory
• Taming release-acquire consistency
• What’s Decidable about Weak Memory Models?
• Brookes Is Relaxed, Almost!
• Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude?
• A unified theory of shared memory consistency
• Verification of Concurrent Programs on Weak Memory Models
• Concurrent Kleene Algebra
• Owicki-Gries Reasoning for Weak Memory Models
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Some Properties of Predicate Transformers
• On the verification problem for weak memory models
• Relaxed memory models
• Software Verification for Weak Memory via Program Transformation
• A promising semantics for relaxed-memory concurrency
• Automatically comparing memory consistency models
• An Efficient Algorithm for Exploiting Multiple Arithmetic Units
• Algebraic models of correctness for microprocessors

This page was built for publication: Parallelized sequential composition and hardware weak memory models