Skip to content

Commit

Permalink
add esop20 paper and acknowledge Arm iCASE
Browse files Browse the repository at this point in the history
  • Loading branch information
bensimner committed Nov 28, 2023
1 parent bcb2063 commit 621d819
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,8 @@ Mainstream Systems" (EP/K008528/1), EPSRC grant "C3: Scalable & Verified
Shared Memory via Consistency-directed Cache Coherence"
(EP/M027317/1), an ARM iCASE award (Pulte), an EPSRC IAA KTF (Gray),
EPSRC Leadership Fellowship "Semantic Foundations for Real-World
Systems" (EP/H005633/1, 2009-2014, Sewell), and EPSRC grant "Reasoning
Systems" (EP/H005633/1, 2009-2014, Sewell), an Arm iCASE Award (Simner),
and EPSRC grant "Reasoning
with Relaxed Memory Models" (EP/F036345, 2008-2012).


Expand Down Expand Up @@ -168,6 +169,11 @@ several concurrency models:
Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan
Lee, and Chung-Kil Hur. In PLDI 2019.

- An extension to the Flat model for Arm to model instruction fetch and the required cache maintenance instructions, described in:

- [ARMv8-A system semantics: instruction fetch in relaxed architectures](https://www.cl.cam.ac.uk/~pes20/iflat/top-extended.pdf).
Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, and Peter Sewell. In ESOP 2020.

### Model validation

These models have been validated against observable hardware behaviour using the litmus tool of the [herdtools](https://github.com/herd/herdtools7) tool suite of Jade Alglave and Luc Maranget; this validation has been done principally by Luc Maranget and Shaked Flur. Some models have also been compared or co-developed with axiomatic models expressed using the herd tool of that tool suite.
Expand Down

0 comments on commit 621d819

Please sign in to comment.