Syntax and analytic semantics of LISA
Jade ALglave, Patrick Cousot
TL;DR
This paper defines the syntax and semantics of LISA, a parallel assembly language used for simulating weak memory consistency models within the herd7 tool.
Contribution
It introduces the formal syntax and semantics of LISA, enabling accurate simulation of weak memory models in the herd7 framework.
Findings
LISA language formalization for weak memory models
Implementation in herd7 simulation tool
Supports analysis of memory consistency behaviors
Abstract
We provide the syntax and semantics of the LISA (for "Litmus Instruction Set Architecture") language. The parallel assembly language LISA is implemented in the herd7 tool (http://virginia.cs.ucl.ac.uk/herd/) for simulating weak consistency models.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsParallel Computing and Optimization Techniques · Software Testing and Debugging Techniques · Model-Driven Software Engineering Techniques