Errata for Simplifying ARM Concurrency:
Multicopy-atomic Axiomatic and Operational Models for ARMv8
Main paper
-
The definition of the coherence relation in the candidate execution
induced by a Flat model trace is incomplete: it is missing a
requirement about the write footprint. For the non-mixed-size case
that the proof covers the definition should read:
(W,W') in co_t
for two same-address writes W and W' if W propagates to
memory before W' in t.
Full Flat model description
The full model text description in the supplementary material is a
revision of an older description; the description incorrectly does not
reflect two changes in the semantics of load/store exclusive
instructions of the formal model (and that the proof assumes).
-
The third condition for the transition Guarantee the success of
store-exclusive has a typo. It should read:
… no slice in wss has been overwritten (in memory)
by a write from another thread, …
where it said … by a write from this thread
…
.
-
The definition for pairing a load-exclusive with a store-exclusive is
incorrect: instead of
A load-exclusive is called successful if the first
po-following store-exclusive that has not been made to fail
has been guaranteed to succeed (…)
the sentence should say
A load-exclusive is called successful if the first
po-following store-exclusive has been guaranteed to succeed
(…)
-
In the definition of the
Finish instruction
transition instead
of
Here a memory write is called fixed if it is the write of
a non-exclusive-store instruction that has fully determined
data.
it should say
Here a memory write is called fixed if it is the write of
a store instruction that has fully determined data.