{'fraction_non_alphanumeric': 0.0591962441977444, 'fraction_numerical': 0.008206992710778517, 'mean_word_length': 3.6053808014305453, 'pattern_counts': {'":': 0, '<': 19, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 33, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Reasoning about Promises in Weak Memory Models with Event Structures (Extended Version)

Modern processors such as ARMv8 and RISC-V allow executions in which independent instructions within a process may be reordered. To cope with such phenomena, so called promising semantics have been developed, which permit threads to read values that have not yet been written. Each promise is a speculative update that is later validated (fulfilled) by an actual write. Promising semantics are operational, providing a pathway for developing proof calculi. In this paper, we develop an incorrectness-style logic, resulting in a framework for reasoning about state reachability. Like incorrectness logic, our assertions are underapproximating, since the set of all valid promises are not known at the start of execution. Our logic uses event structures as assertions to compactly represent the ordering among events such as promised and fulfilled writes. We prove soundness and completeness of our proof calculus and demonstrate its applicability by proving reachability properties of standard weak memory litmus tests.


Introduction
In recent years, numerous works have looked into semantics for weak memory models for various hardware architectures or languages, e.g. for x86-TSO [36], C11 [2,27], Power [35] or ARM [16]. Such semantics typically can be classified as either being declarative (aka axiomatic) or operational. Operational semantics furthermore can be divided into those following a microarchitectural style (providing formalizations of the actual hardware architecture) and those trying to abstract from architectures. Most notably, view-based semantics [14,21,31] avoid modelling specific hardware components and instead define the semantics in terms of views of thread on the shared state. Promises [22,24] are employed in operational semantics as a way of capturing out-of-order writes while still executing operations in thread order. A promise (w.r.t. a value κ and a shared location x) of a thread τ states that τ will eventually write value κ onto location x. All promised writes then need to be fulfilled (i.e., justified) in the future of a program run, but other threads can read from promises before they are fulfilled.
Our interest here is the development and use of Hoare-style [18] structural proof calculi (and their extensions to concurrency by Owicki and Gries [29]) for weak memory models. Owicki-Grieslike proof calculi have been proposed by a number of researchers [11,12,23,41], and have also recently been given for non-volatile memory [3,33]. Svendsen et al. [37] have developed a separation logic for promises for the C11 memory model. Wright et al. [41] have developed an Owicki-Gries proof system for out-of-order writes (as allowed by promises), but rely on pre-processing via the denotational MRD framework [30].
All of these proposals follow Hoare's principle of providing safety proofs. In particular, a Hoare triple p S q describes the fact that an execution of program S starting in a state satisfying p is either non-terminating, or terminates in a state satisfying q (over-approximating the final states). However, for weak memory models, we often want to prove reachability, i.e. under-approximate the set of final states, like in the recent proposal of O'Hearn's incorrectness logic [28]. Here, a triple p S q describes the possibility of program S reaching all states satisfying q when started in a state satisfying p. A verification technique supporting these reachability triples enables one to reason about executions that deviate from the expected sequentially consistent behaviour of concurrent programs. Contributions. In this paper, we present a reachability proof calculus for concurrent programs where the semantics of the weak memory model is based on promises. The specific challenges therein lay in (i) capturing the meaning of promises as writes which will only happen in the future but can nevertheless already be read from, and (ii) appropriately describing the required ordering (and concurrency) between promises and fulfills as fixed by the concurrent program under consideration. We address these challenges via the following contributions. (1) We develop a program logic based on assertions which are (flow) event structures [6, 17,40], employing parallel composition of event structure and synchronization as a means of determining whether all promises read from have eventually been fulfilled. (2) We extend the theory of flow event structures with the notion of a flow label to capture the behaviours observed in weak memory models. (3) We develop the first compositional proof rule for a concurrent reachability (incorrectness) logic. (4) We prove soundness and completeness of this novel event-structure based proof calculus. (5) Finally, we demonstrate its applicability on a number of litmus tests. Overview. In Section 2, we provide a concrete overview via a motivating example and in Section 3, we present the memory model that we use. Our model is a simplified (strengthened) version of the ARMv8/RISC-V semantics of Pulte et al [31]. In Section 4, we present an extended theory for event structures (specifically an extension of flow event structures) that has been designed to enable reasoning about relaxed memory models. We describe our reasoning methodology and provide examples verifying common litmus tests in Section 5.

Motivating Examples
Consider the program in Fig. 1, which describes the load buffering litmus test. Thread 1 (similarly thread 2) loads the value of y (sim. x) into register a (sim. b), then updates x (sim. y) to 1. Since there are no dependencies between lines 1 and 2, and similarly between lines 3 and 4, architectures such as ARMv8 and RISC-V allow the stores in both threads to be reordered with the loads. Thus the program allows the final outcome a = 1 ∧ b = 1. This phenomenon is captured by promising semantics by allowing each thread to "promise" their respective stores, then later fulfilling them. In the meantime, other threads may read from promised writes. Our assertions within a thread reflect this semantics via assertions E which are flow event structures [40]. The events and their partial order reflect program executions, and in particular describe the various views which threads have on shared state.
The proof outlines (i.e., program texts with assertions) of individual threads may first of all contain read events for arbitrary promises, i.e. describe the reading of arbitrary values. In Thread  . . . 5 : dmb; . . . 6 : store y 1 . . .   Fig. 1, the pre-assertion of the load only contains an event for initial writes (labelled ini), yet the load may read the value 1 for y from a promised write, described by the event labelled rd 2 (y, 1) in the post assertion. The semantics generates dependencies if the same register is used (perhaps indirectly) by a read and a later write. This is captured in our assertions using the event labelled bar(a, y), causally ordered after rd 2 (y, 1), which states that the view of register a is at least that of the read of y. Execution of line 2 then adds a fulfill event with label ff 1 (x, 1) to the assertion, which is not ordered with any other event except ini. Symmetric assertions can be generated for Thread 2. To obtain an assertion describing the combined execution, we compose the final event structures of both threads to obtain a "postcondition" of the program. For this, we use parallel composition of event structures, synchronising read with their corresponding fulfill events. In Fig. 1, both reads are valid since the promises that these reads rely on can be fulfilled in the composition without creating cyclic dependencies.  Fig. 1, which includes additional barriers dmb (fences) between the load and store in each thread, preventing their reordering. Again we build a proof outline for an execution in which Thread 1 loads 1 into a, obtaining the assertions shown. Note that here the event structure contains an additional fence event, fnc, that is ordered after bar(a, y) and before ff 1 (x, 1). Similarly, for Thread 2 loading 1 into b, we would obtain a symmetric set of assertions. Here, the parallel composition of local assertions is however not interference free (see below): the promises that threads 1 and 2 have read from cannot be fulfilled in this concurrent program. More detailedly, let E 1 and E 2 below be the (final) event structures of threads 1 and 2, respectively, where ։ arrow denotes ordering and we now give event names together with labels.
The final step in proving is the generation of a valid interference free configuration of the parallel composition, which is a subset of the event structure satisfying certain conditions, including acyclicity of ։, absence of conflicts and absence of unsynchronised reads (ensuring the fulfillment of all promises read from). It turns out that for the event structure above, it is impossible to generate such a configuration. The event (e 1 , * ) cannot be included since it is an unsynchronised read. Therefore, (e 1 , f 4 ) must be included. However, by the definition of a configuration, this also means that the downclosure of (e 1 , f 4 ) must be included, which results in a cycle: f 4 ). Since E 1 E 2 has no interference free configurations, the proof outline is not valid and in fact, a final state with a = 1 ∧ b = 1 is unreachable here.

A Weak Memory Semantics with Promises
We develop a promising semantics inspired by the recent view-based operational semantics by Pulte et al. [31]. We have reduced architecture-specific details, allowing us to focus on the interaction between promises and thread views. Our notion of a promise coincides with earlier works [22,24,31]. Threads can promise to write certain values on shared locations and other threads can read from this promise even before the actual write has occurred. All promises however need to be fulfilled at the end of the program execution.
Syntax. Let x, y ∈ Loc be the set of shared locations, κ ∈ Val the set of values, τ ∈ Tid the set of thread identifiers and a, b ∈ Reg local registers. Our sequential language encompasses the following constructs: rv ::= κ | a st ::= skip | a := load x | store x rv | a := η | dmb S ::= st | S; S | asm β | S + S | S * where η ∈ Exp is an arithmetic and β ∈ BExp is a boolean expressions, both over (local) registers only. We assume S * = ∃n ∈ N. S n , where S 0 = skip and S n = S; S n−1 . We use abbreviations: while β do S = (asm β; S) * ; asm ¬β and if β then S 1 else S 2 = (asm β; S 1 ) + (asm ¬β; S 2 ), where asm β is a command that tests whether β holds.
Timestamped state. We let TState be the set of all timestamped states and Memory the set of all memory states, both of which we make more precise below. A thread T ∈ Thread is an element of S × TState, a concurrent program is a mapping T ∈ TPool = Tid → Thread and a concurrent program state is a pair T , M ∈ TPool × Memory . We let R(τ ), τ ∈ Tid, be the set of registers occurring in the program of T (τ ). We assume R(τ ) ∩ R(τ ′ ) = ∅ whenever τ = τ ′ .
Threads will make promises for writes at particular timestamps. Timestamps t ∈ T are natural numbers. We define t⊔t ′ = max(t, t ′ ) and generalise this to sets of timestamps using t∈T t, where t∈∅ t = 0. A memory is a sequence of write messages of type Wr = (Loc × Val × Tid) ∪ {ini}, where ini is a special write message denoting initialisation. The position of a write in the sequence fixes its timestamp. We assume all variables are initialised with value 0.
We denote a write w = (x, κ, τ ) using x := κ τ and let w.loc = x, w.val = κ and w.tid = τ . For a memory M and thread τ ∈ Tid, we let M τ ⊆ T be the set of timestamps of entries of τ in M , i.e. {t ∈ T | M (t).tid = τ }. M τ is used to determine the promise set of each τ . We write tids(M ) to denote the set of threads with entries in M . New messages w are appended at the end of the memory, which we write as M + + w.
A thread state ts ∈ TState consists of the following components: a set of (non-fulfilled) promises prom ∈ 2 T , a coherence view of each location, coh : Loc → T, the value and view of each register, regs : Reg → Val × T, a read view v read : T, two write views v wOld , v wNew : T and a condition view v C : T. We write regs(a) as κ@v and also let v a be this view v of register a. Finally, the evaluation of an expression η with respect to a register assignment regs, η regs ∈ Val × T, is defined as follows: a regs = regs(a) for a ∈ Reg, η 1 op η 2 regs = (κ 1 op κ 2 )@(v 1 ⊔ v 2 ) with η 1 regs = κ 1 @v 1 , η 2 regs = κ 2 @v 2 Note that this evaluation is with respect to the register function regs and this calculates both the value of the expression and the maximal view of the registers within the expression.
To define the initial state of a program, we let where ts ini is a record initialising the promises to the empty set, each view to 0, the coherence function to a map from locations to timestamp 0, and the register function to a map from registers to value 0 with timestamp 0. We say that a program T is locally in its initial state iff for each thread τ , we have π 2 (T (τ )) = ts ini , where π i projects the ith component of a tuple. Given that T is in its initial state, the initial concurrent program state is given by T , M ini . The rules of the operational semantics (except for standard rules for program constructs) are given in Fig. 3. The two key rules are the Read and Fulfill rule. Read identifies a timestamp t to read a value for x from such that in between t and the maximum of read view and coherence of x, there are no further promises to x in memory M . It updates read view, coherence of x and the view of the register involved in the load as to ensure preservation of dependencies. Fulfill fulfills an already made promise (to write κ to x) of a thread at timestamp t, and to this end has to ensure that views v wNew , v C , coh(x) as well as that of the value/register are less than t. It removes t from the thread's promise set and updates coh(x) and v wOld (as to ensure dependencies with fences). Rule Promise simply adds an arbitrary new promise at the end of memory. Fence ensures views v read and v wNew are updated. This rule for instance guarantees that store operations separated by barriers dmb can only be fulfilled in that order, i.e. the write of the first store cannot be promised to happen later than the write of the second store (more precisely, such promises cannot be fulfilled). Finally, we say that T, M is certifiable (used in Program Step) if there is some T ′ , M ′ such that T, M − → * τ T ′ , M ′ and T ′ .prom = ∅. Certifiability ensures that a concurrent program can only make steps when all promises can eventually be fulfilled. Like [31], in our semantics, all promise steps can be done at the beginning without losing any of the reachable states (see Lemma 1).

Event Structures
Event structures [5,6,17,40] are models of concurrent systems which compactly represent (concurrent) executions. Here, we use flow event structures because of their ease in defining a compositional parallel composition [17].
Notation. Event structures consist of sets of events d, e, f ∈ E. Events will be labelled with actions which are here specific to our usage and give us information about program executions: Actions on a location x can be read actions rd τ (·, ·), fulfill actions ff τ (·, ·) or the initialization ini.
Note that the thread identifier τ in read actions is the id of the thread having made the promise and in fulfill actions it is the thread executing the fulfill (and having made the corresponding promise).
We let Act rd denote all read and Act ff all fulfill actions. To record loading into register a, we use so called bar actions bar(a, ·). The action fnc occurs when a dmb statement is executed and tst · (·) describes the execution of some asm statement. We often lift notations to sets of locations L ⊆ Loc or sets of registers R ⊆ Reg. For example, Act L = x∈L Act x . The overall set of actions is Act = Act Loc ∪ Act Reg ∪ Act fnc ∪ Act tst .
Definition 1. A location-coloured flow event structure (short: event structure) E = (E, ։, #, Λ, ℓ) labelled over a set of actions Act consists of a finite set of events E, an irreflexive flow relation ։ ⊆ E × E, a location restriction function Λ : E × E → 2 Loc , a symmetric conflict relation # ⊆ E × E, and a labelling function ℓ : E → Act.
For L ⊆ Loc, we write e L ։ f to denote e ։ f and Λ(e, f ) = L. The location restrictions are employed to reflect the application condition of rule Read within the event structure: it tells us that there is no write to x ∈ L in between e and f , where e and f will eventually be mapped to timestamps in memory.
We let Ini be the event structure ({e ini }, ∅, ∅, ∅, ℓ) with ℓ(e ini ) = ini. Given an event structure E = (E, ։, #, Λ, ℓ), we -similarly to actions -define its set of events labelled with specific actions as Rd(E), Rd τ (E), Rd x τ (E), Ff(E), Ff τ (E) and Ff x τ (E) via the labelling function ℓ. For an event e labelled with an action in Act x \{ini}, we let e.loc = x. We slightly abuse notation so that e ini .loc = x for all x. We furthermore define last α (E), α ∈ Act, to be the last event in flow order labelled α, i.e., last α (E) = e if ℓ(e) = α and for all e ′ such that e ′ = e and ℓ(e ′ ) = α, we have e ′ ։ + e. Moreover, last α (E) = ⊥ if no event labelled α exists. We lift last to sets of actions by last A (E) = {last α (E) | α ∈ Act}. An event structure E is sequential if all events are flow-ordered: ∀e, e ′ ∈ E, e = e ′ : e ։ + e ′ ∨ e ′ ։ + e. We let S be the set of sequential event structures.
An event structure describes (several) concurrent executions in compact form. One execution is therein given as a configuration.
We let Conf (E) be the set of configurations of E. We identify a configuration with the (conflict-free) event structure E C which is E restricted to events of C.
Our intention is to use event structures to record information about the local history of each thread, in particular the promises of other threads which they have read from. Eventually (i.e., when combining local event structures) all promises read from need to be fulfilled. This is captured by our notion of parallel composition which requires fulfills (of a thread τ ) to synchronize with reads from promises of τ . Similary to CCS [26], we model this synchronisation via complementary actions where rd τ (x, κ) = ff τ (x, κ) and vice versa, and a = a. Contrary to CCS, the synchronisation does not create internal actions, but keeps the fulfill labels (as to still see what promise a fulfill belonged to).
We first define the synchronising events of n event structures E 1 , . . . , E n , as follows, where An event e might also occur unsynchronized in a parallel composition (which is then written as ( * , . . . , * , e, * , . . . , * ).
Note that since we aim to reason about reachability of states (underapproximation), we just need parallel composition for conflict-free event structures, i.e. for event structures describing a single execution. Thus the ∆-axiom of Castellani and Zhang [7] which they impose in order to get compositionality is trivially fulfilled for our application. Next, we still first of all define parallel composition of arbitrary event structures.
We let × i S denote the product S × S × . . . S generating a tuple of length i. If i ≤ 0, we let Definition 3 (Parallel composition). Let E 1 , E 2 , . . . , E n be event structures for threads τ 1 , τ 2 , . . . , τ n , respectively. The parallel composition Parallel composition of event structures is used to combine local proof outlines of threads. This combination is only possible if enough synchronization partners are available. Event structures . . , n} (all the reads have a synchronization with a fulfill). The configuration (describing an execution of the parallel composition of threads) which we extract from Conf (E 1 || . . . ||E n ) furthermore has to guarantee that no events from the local proof outlines are lost and that the local assertions make no contradictory assumptions about the contents of memory.
among reads, fulfills and the ini event such that where e i ∈ Rd(E i ).
Example 1. Consider the two event structures given next (which belong to a message passing program with barriers, see Section 5). e ini : ini e 1 : ff 1 (x, 5) Their parallel composition gives the following event structure: This event structure has no interference-free configuration. To satisfy the conditions "threadcovering" and "no unsynchronised reads", we must include event (e 3 , f 1 ). This means the only possible configuration must also include the downclosure (e 1 , * ) and (e 2 , * ). However, together with the location restriction {x} on the edge ((e ini , f ini ), (e 3 , f 1 )), the resulting event structure is not memory-consistent linearizable, since it contains a sequence ( where (e 1 , * ) corresponds to a fulfilled write on x that is forbidden by the edge ((e ini , f ini ) {x} ։ (e 3 , f 1 )). Conceptually, this means that we cannot find a memory M which matches the constraints on its contents given in the event structure.

Reasoning
Our overall objective is the design of a proof calculus for reasoning about the reachability of certain final states of concurrent programs. A concurrent program state describes the values of registers and shared variables, the contents of memory and the views of threads. During reasoning, we employ event structures as assertions in proof outlines. They abstract from the concrete state in neither giving the exact contents of memory nor the timestamps of thread views.

Semantics of Assertions
Local assertions in the proof outlines of single threads take the form E, where E is a conflictfree event structure (i.e., # = ∅). The event structure is conflict-free because it describes a single execution of the thread (reachability logic). An assertion for a thread τ can have fence and fulfill events of τ , read events reading from (promises of) threads τ ′ = τ as well as bar and test events over registers of R(τ ). The events in E -together with some memory M -allow us to compute the current views of threads. Figure 4 gives some definitions for calculating views.
A local assertion of a thread τ defines constraints on the global memory M (the ordering of writes and their values) as well as the views of τ : An assertion E describes a set of states E = { ts, M ∈ (Tid → TState) × Memory | ts, M matches E} where "matches" is defined by conditions (1)-(4) below.
(1) M is consistent with the fulfill and read events of E. There exists a total mapping ψ : 1. initializes at zero: the one event e ini labelled ini is mapped to 0, 2. is consecutive for every thread τ : , 5. and preserves memory constraints: The mapping ψ is used to assign timestamps to read and fulfill events. We therefore will later also talk about the timestamp of an event (depending on such a mapping). Note that the event structure Ini is consistent with all memories M (using mapping ψ(e ini ) = 0).
(3) The views of a thread τ are consistent with mapping ψ and M . Letting ts = ts(τ ), a ∈ R(τ ) and x ∈ Loc, we have For a ∈ Reg, ts.regs(a) = κ@v a with κ = a E (where the semantics of a register a in E is (1) 0 if no bar event for a is in E or (2) the value of a read or fulfill to x prior to the last bar(a, ·) (on x) or (3) the value of the expression η in a last bar(a, η)) and v a as defined above. Figure 5 gives an example for the definition of "matches". On the right hand side we see the program of thread 1. It first stores 1 to y, then loads the values of y and x into registers a and b, respectively, and finally stores 3 to z. The event structure in the middle gives the assertion reached after statement 3, i.e. before the final store operation. The memory M on the left hand side matches this event structure: There are promises for the event ini at M (0) as well as for event ff 1 (y, 1), so ψ . . .
Thread 1 1 : store y 1; 2 : a := load y; 3 : b := load x; 4 : store z 3; maps ini to 0 and ff 1 (y, 1) to 6. The colored location restriction in the event structure furthermore requires not to have any promises to x in between 0 and 6. As there is one more promise of thread 1 in M , not yet covered by the event structure, we can derive 1.prom = {9}.

Proof Rules
Essentially, assertions describe the events which have already happened together with their orderings plus further constraints. The initial assertion in proof outlines is always the event structure Ini. Then, the proof rules successively add new events to the event structure when e.g. reading from or writing to shared variables. We however never add events for promises; rather, threads can first of all assume arbitrary promises of other threads having been made which they can read from. The overall interference freedom constraint guarantees that these local assumptions about promises are met at the end.
For adding new events, we use a number of ⊕-operators, detailed in Fig. 6. The event structures in there are local to threads and describe a single execution of the thread, hence are conflict-free. The definition of these operators has to ensure that they capture the dependencies between views as defined by the operational semantics. For example, rule Fulfill requires (among others) the PR-Write PR-IterateZero timestamp t to be larger than control view v C , hence E ⊕ ff τ (x, κ) has to introduce a flow from the last test event to the newly added fulfill event. Figure 7 gives the proof rules for building local proof outlines of threads. Most of the rules (i.e., PR-Write, PR-WriteR, PR-Fence, PR-Registers and PR-Assume) just add one new event to the event structure recording the occurrence of a particular program statement. More complex are the two read rules: PR-ReadEx is applied for load statements reading from x when the event structure already contains an event e describing (in the sense of E ) the entry in memory to read from; this can be a read, fulfill or the ini event. In this case, the event structure after the load has to reflect the applicability condition of rule Read: no entries in memory to x in between t (the timestamp of e in E ) and v read ⊔ coh(x). This is achieved by inserting an additional location restriction x via the operator rstr x e (E) to the following (potentially already L-labelled) flows (thus getting the restriction L ∪ {x}): Rule PR-ReadNew on the other hand introduces new read events into an event structure upon a load statement. The rule can directly introduce an entire sequence of read events (i.e., add a sequential event structure E ′ ) as to enable later reads from memory entries which are prior to the entry of the current read (described by event e in the rule). This is required for message passing idioms like in the following program.
Thread 1 1 : store x 5; 2 : dmb; 3 : store y 1; Thread 2 4 : a := load y; Here, due to the fence in Thread 1, Thread 2 -after having read y to be 1 -can only read x to be 5. When constructing the proof outline for Thread 2, we need to apply rule PR-ReadNew for the first load giving us ini ։ rd 1 (x, 5) ։ rd 1 (y, 1) ։ bar(a, y) as assertion after statement 4. For the subsequent load we can then apply proof rule PR-ReadEx.
Note that we could also construct a local proof outline having the load in line 4 read from ini. This would then give us the two event structures of Example 1 which we, however, have already seen to not allow for an interference free configuration of their parallel composition. Finally, we have a proof rule for parallel composition which combines local event structures when they are synchronisable and the resulting configuration is interference free.
This rule ensures that (1) all synchronization constraints are met (i.e., the promises that threads want to read from have been made) and (2) there is a configuration C of the combined event structure which is interference free.
Example 2. Next, we give a complete proof outline for the message passing litmus test without a barrier in the writing thread. We see that here message passing is not guaranteed (i.e., reading y to be 1 does not "pass the message" that x is 5 from Thread 1 to 2) and we can actually reach a final state with a = 1 ∧ b = 0 (as calculated by a E and b E taking the value of the last fulfill or ini event prior to the last bar event on a and b, respectively).

Soundness and Completeness
Due to lack of space, we can neither discuss soundness nor completeness of our proof calculus in some more detail here. Proofs can be found in the appendix.
Soundness requires proving all local proof rules correct plus showing the correctness of rule Parallel as of Theorem 1 below. It states that whenever we find an interference free configuration in the parallel composition of synchronizable event structures in a locally sound proof outline, all thread states and memory contents matching this configuration are actually reachable by the concurrent program.
. . , n}, be proof outlines of threads τ 1 to τ n such that E 1 to E n are synchronizable and let T 0 be an initial thread pool with T 0 (τ i ) = (S i , ts ini ) and M 0 = M ini .
Our second main result is the completeness of the proof calculus: whenever there is an execution of a concurrent program, our proof calculus allows to show the reachability of its final state. More specifically, for every trace of a concurrent program we find local proof outlines with synchronizable event structures and an interference free configuration describing the final state of the trace.
Then there are local proof outlines [Ini] S k [E k ] of threads τ k , k ∈ {1, . . . , n}, such that E 1 to E n are synchronizable and there exists an interference free configuration C ∈ Conf (E 1 || . . . ||E n ) with T , M ∈ E C .

Related Work
The first semantics of weak memory models employing promises has been proposed by Kang et al. in 2017 [22] for building an operational semantics which allows modelling of read-write reordering while at the same time disallows out-of-thin-air behaviours. Our semantics here is a slightly simplified version of the promising semantics of ARMv8 given by Pulte et al. [31]. In particular, like [31] all program traces can be reordered so that the promise steps are all at the beginning which is a key property required for the soundness of our proof calculus.
There are already several proposals for program logics for weak memory e.g. [1,10,11, [13][14][15]23,34,38]. The only one explicitly dealing with promises in the semantics is the proposal of Svendsen et al. [37]. They develop a safety proof calculus whereas we are interested in reachability. Their logic furthermore has to deal with promises occurring at any program step (as they show soundness with respect to the promising semantics of [22]), whereas we rely on all promises being made at the beginning.
Partial order models of concurrency have already been used for giving the semantics of memory models [8, 19,20], but not for reasoning. Wright et al [41] take the approach of using a semantic dependency relation, which is a partial order generated through an event structure representation of a C/C++ program [30], which is a partial order over a thread's execution. An Owicki-Gries logic is provided to reason directly over such partial orders. Incorrectness logic as used for proving reachability properties of sequential programs has been introduced by O'Hearn [28], with a predecessor approach with (almost) the same principles by de Vries and Koutavas [39]. The first extension of incorrectness logic to concurrent programs has been proposed by Raad et al. in the form of an incorrectness separation logic [32] which is however not compositional.
Colvin [9] defines a semantics based on a reordering relation for several hardware memory models, which is then lifted to a Hoare calculus. This is then rephrased into a reachability property by defining triples p s q = ¬{p} s {¬q}, which states that it is possible for s to reach q if execution starts in a state satisfying p. Note that this is weaker than O'Hearn's notion of incompleteness, which states that all states satisfying q are reachable from an execution starting in a state satisfying p.

Conclusion
In this paper, we have proposed a reachability (incorrectness) logic for concurrent programs running on weak memory models. The reasoning technique is based on assertions which are event structures abstractly describing the contents of memory and the views of all threads. We have proven soundness and completeness of the proof calculus, and have demonstrated its applicability by proving the outcomes of some standard litmus tests to be reachable.

RRC -Read Read Coherence
In the read read coherence litmus test the first two threads store different values to x, while the other two threads load x into different registers. The outcome a = 1 ∧ b = 2 ∧ c = 2 ∧ d = 1 ✗ should not be allowed and indeed, the parallel composition of local proof outlines does not give us an interference-free configuration. Here, we also give the event names in the assertions.
WRC -Write-to-Read Causality The next litmus test is the WRC example, originally formulated by Boehm and Adve [4] and appearing here in the form of [25].
SB -Store buffering Next, we take a look at the standard SB example. We see that the outcome a = 0 ∧ b = 0 ✓ which is possible in lots of weak memory models is also possible here, and can be proven to be reachable.

IRIW -Independent Reads of Independent Writes
In the IRIW litmus test we have two threads writing to shared variables x and y, respectively, and two other threads both reading both variables, but in a different order. The outcome a = 1 ∧ b = 0 ∧ c = 1 ∧ d = 0 ✗ is not allowed by our semantics.
Thread 1 ini store x 1; ini ։ ff 1 (x, 1) And indeed, while we can construct local event structures for each thread, the one candidate for a configuration of their parallel composition is  But this configuration is not interference free (because of the location restrictions there is no valid linearization of the read and fulfill events), and we hence (correctly) cannot show outcome a = 1 ∧ b = 0 ∧ c = 1 ∧ d = 0 ✗ to be reachable.

B.1 Properties of the Operational Semantics
We start with two properties of the operational semantics. The first ensures that in any trace, the promises can be reordered so that they are executed at the start of the trace without affecting the final outcome.
Lemma 1. For every trace tr there exists a trace tr ′ (ending in the same final state) such that in tr ′ all promise actions of tr occur at the beginning followed by the non-promise actions of tr (in the same order as in tr).

Proof. Let
be a trace tr with I = {i | op i = rd · (·, ·)} being the set of all promises. Let i 1 < i 2 < ... be the elements of I. We now want to swap op i1 with the operation before it, until op i1 is the first one in the trace. After that we do the same with op i2 until it is the second operation and so on. For that we need to show that we can swap a promise with a fence, fulfill or read operation before it.
Let op i be a promise operation, l its location and op i−1 the operation in front of op i . If we promise something, we change prom to prom ∪ {|M i−1 | + 1} in ts and add one element to the memory. In case that op i−1 is a fence operation we can reorder op i and op i−1 , because a fence operation changes different attributes of ts (v read and v write ) and has no effects on the memory.
If op i−1 is a fulfill operation, it fulfills a different promise. Hence the condition v write ⊔ ts.coh(l) ⊔ v a < t still applies after the reordering, because t depends on the promise op i−1 is fulfilling. The changes of coh and v write are not related to the changes caused by op i . Additionally the element deleted by op i−1 in prom is not the same as the element that op i adds. So we can also reorder a promise and a fulfill.
In case that op i−1 is a read operation, op i−1 changes other attributes of ts then op i would. If op i−1 reads from a location l ′ , which is different from l, the condition ∀t ′ . t < t ′ ≤ (ts.v read ⊔ ts.coh(l)) ⇒ M (t ′ ).loc = l holds. However, when op i−1 reads from l, we need to have a deeper look at v read and coh. Both will only be replaced by timestamps of entries in M i−1 . Those timestamps are always smaller then |M i−1 | + 1, so the condition is still true. Hence we can reorder a read and a promise operation.
That means we can reorder the operations of our execution in a way that all promises are at the beginning and the final state stays the same.
The second property ensures that views of each component monotonically increase after each transition. Note that this differs from the semantics of Pulte et al., where register views might decrease after the execution of a write to a local register [31].
Since v read changes whenever v wN ew does and both are set to the same value we get ts.v read ≥ ts.v wN ew . Therefore ts ′ .v wN ew ≥ ts.v wN ew . -For regs(a) = κ@v a we first show that ts.v a ≤ ts.v read is an invariant. We know that v a only changes for op = rd(x, κ) and op = lst(a, exp) whereas v read changes for op = rd(x, κ) and op = fnc. For op = rd(x, κ) v a and v read are set to the same value. Since ts ′ .v read ≥ ts.v read , v a can not get bigger than v read after a register operation. Therefore our invariant holds and we get: , exp) changes v a to the maximum of v a and the view of exp., ts ′ .v a ≥ ts.v a

B.2 Soundness
Next we prove soundness of our proof rules. We first prove correctness of each of the atomic rules from Fig. 7.
Proposition 2 (Soundness of rule PR-WriteR). Let ts ′ , M ∈ E ⊕ a ff τ (x, κ) and a E = κ. Then there exists ts, M ∈ E such that store x a, ts , M − Proof. We write E ′ for E ⊕ a ff τ (x, κ). Let ts ′ , M ∈ E ′ and let e ′ be the event such that ℓ(e ′ ) = ff τ (x, κ) This means that there exists some mapping ψ ′ : ts, M satisfies E ′ . In particular, ψ ′ (e ′ ) = t implies that M (t) = x := κ τ . We show that there exists some ts, M ∈ E such that the following holds (eliding the program statements): Note that M is unchanged and t in the rule Fulfill is instantiated to ts ′ .coh(x). We define ts to be the following by using ψ ′ : ψ(e) logic 4. Trivial since no register value is modified.
Recall that ts.v C = e∈prTst τ (E) ψ(e). By definition of E ⊕ a ff τ (x, κ), we have that the event corresponding to ff τ (x, κ) is causally after each e ∈ prTst τ (E). Thus ts.v C < ts ′ .coh(x). • ts.coh(x) < ts ′ .coh(x) because by definition of E ⊕ a ff τ (x, κ) we have a causal edge from each e ∈ Act x to the event corresponding to ff τ (x, κ). • ts.v a < ts ′ .coh(x) same Because Proof. For the proof, we elide the program statements. We write E ′ for rstr x e (E ⊕ bar(a, x)). Let ts ′ , M ∈ E ′ . This means that there exists some mapping ψ ′ : Ff(E ′ ) ∪ Rd(E ′ ) ∪ {e ini } → dom(M ) such that ψ ′ can be used to show that ts ′ , M satisfies E ′ , in particular by preservation of memory constraints for the location-restricted red flows for all timestamps t ′ , events f such that ψ ′ (e) < t ′ < ψ ′ (f ) and e ։ f and f ∈ (prFnc τ ( .loc = e.loc. We now show that there exists some ts, M ∈ E such that Note that M stays the same as we do not have any further promises. We define ts to be the following (using ψ := ψ ′ ): ts.v read := e∈(prFnc τ (E)∩Ffτ (E))∪prBar τ (E) ψ(e) ts.v C := ts ′ .v C Since E ′ neither has additional fulfill nor read events nor fences nor tests and M is the same and prFnc τ (E) = prFnc τ (E ′ ), we by definition get ts, M ∈ E . Next, we need to determine the timestamp t for reading, which in this case is ψ(e). Since ψ preserves contents and ℓ(e) ∈ {rd τ (x, κ), ff τ (x, κ), ini}, we get M (t).loc = x and M (t).val = κ (κ = 0 in case of reading initial values). Now consider some timestamp t ′ such that t < t ′ ≤ ts.v read ⊔ ts.coh(x). Let f be the event such that ψ(f ) = ts.v read ⊔ ts.coh(x). This implies (definition of ts.coh(x) and . By preservation of memory constraints we thus have M (t ′ ).loc = e.loc.
Next to the views. We need to show the correct afterstate for three views being changed by the read rule: v a , coh(x) and v read .
v a is set to ts.v read ⊔ t. We get as ⊕ in particular introduces a flow between the event read from (which is labelled with some action in Act x ) and other bar events to the event bar(a, x).
This holds as the new bar event is flow after all other bars and all fences (by definition of ⊕).
= ts ′ .v read -Finally, we look at the value in register a which is set to κ (which is M (t).val). a E ′ = κ as the reading event e is in last Act x (E ′ ) (as this is equal to last Act x (E) and reading from last events is required by the hypothesis of rule PR-ReadEx) and the event is in prBar a (E ′ ) (by definition of ⊕).
Proposition 4 (Soundness of rule PR-ReadNew). Let ts ′ , M ∈ (E ⊕ E ′ ) ⊕ bar(a, x) , E ′ as of rule PR-ReadNew. Then there exists ts, M ∈ E such that a := load x, ts , M − Proof. For the proof, we elide the program statements. We write E after for (E ⊕ E ′ ) ⊕ bar(a, x). Let ts ′ , M ∈ E after . This means that there exists some mapping ψ ′ : Ff(E after ) ∪ Rd(E after ) ∪ {e ini } → dom(M ) such that ψ ′ can be used to show that ts ′ , M satisfies E after . Let e be the event in E ′ which we read from and let t = ψ ′ (e). We set ts to be the thread state which we construct from E and M using ψ for which we take ψ ′ | E . By definition of E after , e is flow-after all fulfills of x, all fences plus reads in E which are followed by a bar event (and e not in E). As ψ ′ is preserving flows, all events f ∈ (prFnc τ (E) ∩ Ff τ (E)) ∪ prBar (E) (which determine ts.v read ) have a timestamp less than t, hence ts.v read < t. Similarly, all events f ∈ Ff x τ (E) ∪ prBar x τ (E) (which determine ts.coh(x)) have a timestamp less than t and hence ts.coh(x) < t. Hence the condition of the read rule in the operational semantics about locations is trivially fulfilled. Moreover, v post is t. Thus, v a as well as v read and coh(x) are set to t, and this then coincides with ts ′ .v a , (as ts ′ .v a = f ∈prBar a (E af ter ) ψ ′ (f ) and e is the maximal event in this set), with ts ′ .v read (similarly, because e is the maximal event in (prFnc τ (E af ter ) ∩ Ff τ (E af ter )) ∪ prBar (E af ter ) and with ts ′ .coh(x) (similarly, because e is the maximal event in Ff x τ (E af ter ) ∪ prBar x τ (E af ter )), respectively. Views v wOld , v wN ew and v C keep their values as of the operational semantics, and indeed calculating their views from E and E af ter gives the same value as we neither introduce new test events (this would change v C ) nor new fulfills (would change v wOld ) nor fences (would change v wN ew ).
Finally, we look at the value in register a which is set to κ (which is M (t).val). a E after = κ as the reading event e with label rd τ ′ (x, κ) is in last Act x (E after ) ∩ prBar a (E after ).
Proof. For the proof, we elide the program statements. We write E ′ for E ⊕ fnc τ . Let ts ′ , M ∈ E ′ . This means that there exists some mapping ψ ′ : Ff(E ′ ) ∪ Rd(E ′ ) ∪ {e ini } → dom(M ) such that ψ ′ can be used to show that ts, M satisfies E ′ . We now show that there exists some ts, M ∈ E such that ts, M − fnc − → τ ts ′ , M Note that M stays the same as we do not have any further promises. We define ts to be the following by using ψ := ψ ′ : Since E ′ neither has additional fulfill, read nor bar events, M is the same and prBar τ (E) = prBar τ (E ′ ) is the same, we by definition get ts, M ∈ E . Next to the views. We need to show the correct afterstate for two views being changed by the fence rule: v wN ew and v read . Both are set to ts.v read ⊔ ts.v wOld .
-For v read we get as ⊕fnc τ introduces a flow from all last events to the new fence and so Ff τ as prBar τ (E ′ ) and Ff τ (E ′ ) are subsets of prFnc τ (E ′ ). -For v a we get as ⊕bar(a, exp) introduces for every b ∈ R(exp) ∪ {a} a flow from the last bar(b, ·) to bar(a, exp) and so prBar a (E ′ ) = prBar a (E) ∪ a ′ ∈R(exp) prBar a ′ (E). Proof. For the proof, we elide the program statements. We write E ′ for E ⊕tst τ (bexp). Let ts ′ , M ∈ E ′ . This means that there exists some mapping ψ ′ : Ff(E ′ ) ∪ Rd(E ′ ) ∪ {e ini } → dom(M ) such that ψ ′ can be used to show that ts ′ , M satisfies E ′ . We now show that there exists some ts, M ∈ E such that ts, M − Note that M stays the same as we do not have any further promises. We define ts to be the following by using ψ := ψ ′ : We take ts.v := ts ′ .v for all views except for v C . For the control dependence view v C we take ts.v C := e∈prTst τ (E) ψ(e). Moreover, we let ts.regs(a) = κ a @ts.v a where κ a = a E . Note that ts ∈ E . Furthermore, since bexp E = true (precondition of proof rule for assume), we get bexp ts.regs = true@v for v = v a1 ⊔ . . . ⊔ v am such that R(bexp) = {a 1 , . . . , a m }. Hence the transition asm(bexp) is enabled in ts. It remains to be shown that we reach ts ′ by taking this transition. The interesting case is v C : In addition, we need to (define and) show the soundness of the proof rule Parallel. This is a bit more complex. We start with two propositions on the existence of memories and on thread states belonging to combined and individual event structures.
Proof. Let C be an interference free configuration of E 1 || . . . ||E n . Let ≺ be the total memory consistent linearizable order. We assume it to be e ini ≺ e 1 ≺ . . . ≺ e m for E C = {e ini , e 1 , . . . , e m }. We now construct the following memory M : With this, we let ψ map e ini to 0 and e i to i. By construction and C being interference free, ψ is (i) initializing at zero, (ii) consecutive, (iii) content preserving, (iv) flow preserving, and (v) memoryconstraints preserving. The thread states ts 1 , . . . , ts n can then simply be calculated from M , ψ and C.
The second proposition is a sort of compositionality result of parallel composition with respect to the global state (views and memory) of a program and its projection onto the threads and their individual proof outlines.
Proposition 9. If E 1 to E n are synchronizable and C is an interference free configuration of Conf (E 1 || . . . ||E n ), then ts i , M ∈ E C implies ts i , M ∈ E i , i ∈ {1, . . . , n}.
These two propositions next help us to establish our first main result which is the soundness of the rule of parallel composition.
. . , n}, be proof outlines of threads τ 1 to τ n such that E 1 to E n are synchronizable and let T 0 be an initial thread pool with T 0 (τ i ) = (S i , ts ini ) and M 0 = M ini .
Proof. Note first that by Proposition 8 such states ts i , M always exist for interference free configurations.
For the proof, we basically show the existence of an execution of this form: First note, that Lemma 1 tells us that such a trace which first executes all promises and then the remaining operations exists. We first show T 0 , M 0 − → * T p 0 , M . For this, we let T p 0 be the thread pool coinciding with T 0 except for the promise sets which are ts i .prom = M τi , i ∈ {1, . . . , n}. Assume #M = m, M (j) = x := κ τ and let op j = prm τ (x, κ), 1 ≤ j ≤ m. Then (promises are made in the order as given by M ) and all these steps are certified as the promises will finally be empty. Next, we consider the steps of statements. For this, first let ts p i be T p 0 (τ i ).tstate be the state of thread τ i after having made the promises.
These steps now have to be lifted to program steps of the parallel program. We construct a sequence of thread pools T 0 1 , . . . , T k1 1 , . . ., T 1 n , . . . , T kn n sequentially executing all thread programs by letting Note that T p 0 = T 0 1 and T = T n kn . As ts i .prom = ∅, all program steps are certified and we get

B.3 Completeness
Finally, we prove completeness of our proof calculus. We must prove that for every trace of a program we can construct local event structures, whereby the parallel composition of the local event structures contains an interference-free configuration. We construct these local event structures by induction following the execution trace.
Then there are local proof outlines [Ini] S k [E k ] of threads τ k , k ∈ {1, . . . , n}, such that E 1 to E n are synchronizable and there exists an interference free configuration C ∈ Conf (E 1 || . . . ||E n ) with T , M ∈ E C .
For the proof, we need a number of well-formedness conditions on the event structures our proof rules construct. First of all, we slightly extend the action labels of events: instead of rd τ (x, κ) we use rd t τ (x, κ) to denote the timestamp t of the read value in memory, and we similarly use ff t τ (x, κ). In a trace tr = T 0 , M 0 − op1 −− → . . . − op2 −− → T , M we define T rd (tr, τ ) to be the set of timestamps that thread τ reads from, similarly T ff (tr, τ ) for the timestamps of the fulfills. With these extensions at hand, we say that an event structure E = (E, ։, #, Λ, ℓ) of thread τ is timestamp closed if the following holds: ∀t, t ′ ∈ T rd (tr, τ ), e ∈ E, if ℓ(e) = rd t · (·, ·) and t ′ < t, t ′ = 0, then there exists an e ′ ∈ E with ℓ(e ′ ) ∈ {rd t ′ · (·, ·), ff t ′ τ (·, ·)}; E is timestamp ordered if ∀t, t ′ ∈ T rd (tr, τ ) ∪ T ff (tr, τ ) we have: if t ′ < t, then t ′ -labelled events cannot be flow-after t labelled events; E contains a modification order for all locations x if for all x ∈ Loc, ։ + | Act x ×Act x is a total order. Finally, we need some conditions on the read events occuring in the event structures. Recall that the rule PR-ReadNew may introduce a number of read events (ordered in a chain) of which only the last in the chain is used for reading at that time. This reading is marked by attaching a bar event flow after the read. We define a read event e in E to be unbarred, ubr E (e), if ℓ(e) = rd · (x, ·) ∧ ¬∃e ′ s.t. ℓ(e ′ ) = bar(·, x) ∧ e ։ E e ′ . We say that all read chains end in a bar in E if the following holds: ∀e ∈ E : ubr E (e) ⇒ ∃m, ∃e 1 , . . . , e m ∈ Rd(E), e 1 = e, e i ։ E e i+1 ∧ ¬ubr(e m ).
Proof. Assume tr : T 0 , M 0 − op1 −− → T 1 , M 1 . . . − opm −− → T m , M m = T , M is the trace such that all promises are done at the beginning, and let op j be the last such promise operation leading to T j , M j . Note first that M j = M j+1 = . . . = M m = M (only promises change the memory). We now inductively construct the event structures E i k of every thread k, 1 ≤ k ≤ n (and by this the proof outlines) for all indizes i = j to m. In every step, the event structures E i k are (i) timestamp closed, (ii) timestamp ordered, (iii) contain a modification order, (iv) all read chains end in a bar and moreover (v) T i (τ k ), M ∈ E i k using the mapping ψ : Ff(E i k ) ∪ Rd(E i k ) ∪ {e ini } → dom(M ) to be e ini → 0 rd t · (·, ·) → t ff t · (·, ·) → t Induction Start i = j: E i k = Ini. As the event structure Ini contains just a single event, it is timestamp closed, timestamp ordered and contains a modification order. Moreover, T j (τ 1 ), M ∈ Ini because the event e ini gets mapped to 0 by ψ, and hence all views are 0, and the promise set contains all entries in M of τ 1 .

Induction
Step Assume E i k with properties (i) to (iv) has been constructed. We now have different cases depending on the next operation op i+1 . Let T i (τ k ) = (S i , ts i ).
1. op i+1 is not an operation of τ k : Then E i+1 k = E i k . As the event structure is not changing and the state of thread τ k is not changing, all properties are trivially preserved. 2. op i+1 = dmb is an operation of thread τ k : Then E i+1 k = E i k ⊕ fnc τ k . As the new event is neither a read nor a fulfill (which would have timestamps), event structure E i+1 k is still timestamp closed, timestamp ordered, contains a modification order and all read chains end in bar. As for the views: there are two views affected by the fence operation, v read and v wN ew . We only consider these here. First, v read . By the operational semantics, we know that ts i+1 .v read = ts i .v read ⊔ ts i .v wOld . We need to show that this fits to the semantics of E i+1 k given the semantics of E i k and operation ⊕.
The last term corresponds to ts i+1 .v read when calculated from E i+1 1 . For v wN ew we get almost the same reasoning as the new fence event is placed flow after all but test events. 3. op i+1 = ff τ k (x, κ) is an operation of thread τ k : By the operational semantics, this transition results from a statement store x a for some register a such that ts i .regs(r) = κ@v a . Let t be the timestamp of the promise in M being fulfilled, i.e. t ∈ ts i .prom. Since T i (τ k ), M i ∈ E i k (by induction hypothesis), we get a E i k = κ. Hence proof rule Write is applicable and we let E i+1 k = E i k ⊕ a ff t τ k (x, κ). We show properties (i) to (v). By induction hypothesis, E i+1 k is timestamp closed as the additional event is not a read event. It is timestamp ordered as the new event is added flow after all events e ′ with ℓ(e ′ ) ∈ Act x , and we know by the operational semantics that ts i .coh(x) < t, and by E i k that ts i .coh(x) is the maximum of all fulfills and reads to x. It moreover maintains the existence of a modification order for x due to the same reasons. All read chains end in bar because no new reads are added. Next to the state after the fulfill: the operational semantics changes the view coh(x) and v wOld as well as prom and keeps the rest. We need to show that this after state is in E i+1 k . First, coh(x) = t (by operational semantics) and this would be derived from E i+1 k as the new event ff t τ k (x, κ) is maximal on all x-labelled events. Also, since this event is now in the event structure, t is not in prom anymore. Finally, v wOld is derived from the event structure as the maximum of all timestamps of fulfills. This includes t and hence v wOld := v wOld ⊔ t holds. For the remaining views: v C is unchanged because no new test events are added; v wN ew is unchanged because no fence is added; all v a 's are kept as no bar events are added and v read is unchanged as neither fences nor bars are added. 4. op i+1 = lst(a, exp) is an operation of thread τ k : Then E i+1 k = E i k ⊕ bar(a, exp). As the new event is neither a read nor a fulfill, E i+1 k is still timestamp closed, timestamp ordered, contains a modification order and all read chains end in bar. Further exp E = exp ts i+1 .regs @v for some view v and ts i+1 .v a = e∈prBar a (E i+1 k ) ψ(e). Both equations follow directly from the construction in the proof of Proposition 6. 5. op i+1 = asm(β) is an operation of thread τ k : Since T i (τ k ), M i ∈ E i k and β ts i .regs = true@v, for some view v, we get β E i k = true. Hence proof rule Assume is applicable and we let E i+1 k = E i k ⊕ tst τ k (β). As the new event is neither a read nor a fulfill, E i+1 k is still timestamp closed, timestamp ordered, contains a modification order and all read chains end in bar. Now we only need to show that ts i+1 .v C = e∈prTst τ k (E i+1 k ) ψ(e) which follows directly from the construction in the proof of Proposition 7. 6. op i+1 = rd(x, κ) is a transition of thread τ k executing instruction a := load x thereby reading from timestamp t: Let T = {t 1 , . . . , t q } be the set of timestamps that thread τ k will read in tr after and including op i+1 for which there is furthermore no timestamp in T ff (tr, τ k ). Let T ≤t = {t ′ ∈ T | t ′ ≤ t} and let t 1 < t 2 < . . . < t p be an ordering of that set. Note that t p = t. By timestamp closedness, there is some index ℓ, 0 ≤ ℓ ≤ p, such that all timestamps t ′ ∈ T rd (tr, τ k ) with t ′ ≤ t ℓ have read or fulfill events in E i k . Two cases need to be considered: If ℓ = p, i.e. read or fulfill events for all T ≤t are in E i k , we apply rule PR-ReadEx. We let e ′ = last Act x (E i k ). By existence of a modification order, e ′ is uniquely defined. We need to show that the timestamp of e ′ is t. Assume the contrary, i.e. e ′ has a timestamp t ′ = t. Let e be the event in E i k with timestamp t. e is also an event on location x, i.e. by modification order and e ′ ∈ last Act x (E i k ), we have to have e ։ + e ′ . By timestamp ordering, we thus have t < t ′ . By the operational semantics, we get t ′ > ts i .v read ⊔ ts i .coh(x). As ts i , M ∈ E i k , e ′ has to be an unbarred read (because in case of a fulfill, ts i .coh(x) ≥ t ′ ; in case of a barred read ts i .v read ≥ t ′ ). However, in E i k all read chains end in a bar, hence ts i .v read is greater or equal the timestamp of the last event in the chain, and hence greater or equal t ′ . Contradiction. Hence the timestamp of last Act x (E i k ) is t.