Mathias Weber
email: mweber@cs.uni-kl.de

Annette Bieniusa
email: bieniusa@cs.uni-kl.de

Arnd Poetzsch-Heffter

EPTL -A Temporal Logic for Weakly Consistent Systems (Short Paper)

The high availability and scalability of weakly-consistent system attracts system designers. Yet, writing correct application code for this type of systems is difficult; even how to specify the intended behavior of such systems is still an open question. There has not been established any standard method to specify the intended dynamic behavior of a weakly consistent system. In this paper, we present a event-based parallel temporal logic (EPTL), that is tailored to specify properties of weakly consistent systems. In contrast to LTL and CTL, EPTL takes into account that operations of weakly consistent systems are in many cases not serializable and have to be treated respectively to capture their behavior. We embed our temporal logic in Isabelle/HOL and can thereby leverage strong semi-automatic proving capabilities.

Introduction

To improve availability and fault tolerance, information systems are often replicated to several nodes and globally distributed. In such system scenarios, designers face a trade-off between availability, fault tolerance, and consistency. To achieve high availability, designers might weaken the consistency constraints between the nodes. In weakly consistent systems, we might refrain from making the objects consistent after each operation. For example, the replicated state might consist of several objects and communication is done via asynchronous message passing.

In such systems with weak consistency semantics, concurrent modifications of a replicated object can lead to a divergent system state as the order in which updates are applied can differ among the nodes. To avoid the divergence, these update conflicts need to be resolved e.g. using CRDTs [START_REF] Shapiro | Conflict-free replicated data types[END_REF]. The main idea of CRDTs is to leveraging mathematical properties of the data structure and its operations to automatically solve conflicts due to concurrent modifications of the replicated object state.

The standard notion of time as being linear is known to not work well in weakly consistent systems [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]. Instead of assuming linear time, we follow Burckhardt et al. [START_REF] Burckhardt | Replicated data types: Specification, verification, optimality[END_REF] in representing time as a partial order on the events in the system.

The topic of specifying weakly consistent systems is an open research question. LTL [START_REF] Pnueli | The temporal logic of programs[END_REF] is a classical specification language for dynamic properties of systems. It is widely used to specify properties of reactive systems. LTL is known for formulas which are easy to understand as well as its formal foundation. As we will show in Section 2, it can be difficult to capture the concurrent nature and asynchronous communication typical for weakly consistent systems in LTL (and CTL).

We want to decouple the specification of the behavior of the system from the behavior of the data types and want to enable to choose among different implementations based on the required properties described in the system specification. Our focus is on the understandability of the specification as well as a solid formal foundation.

Abstract executions Our goal is to have a specification language for properties of weakly consistent systems. The specification should be independent of the conflict resolution strategy used in the concrete implementation because this strategy partially depends on the required properties.

Weakly consistent systems are composed of multiple processes. Instead of sharing the state directly and protecting concurrent accesses using locks, each process obtains a replica of the shared object and solely interacts with this object. The values of the replicas are synchronized by asynchronously distributing the operations to all replicas. A typical data structure used in such systems is a multi-value register (MVR). This datatype ensures that all written values of concurrent write operations are visible to subsequent read operations. The put operations allows to assign a new value to the register, the get operation allows to access the current state. Since the result of the get operation can consist of multiple concurrently written values, the operation returns a set of values. This means that if concurrently we have an operation writing the value 1 and one operation writing the value 2, the value of the register after synchronization of the operations is the set {1, 2}. Note that this property of multi-value registers usually leads to non-serializable system traces.

When formally specifying the semantics of the multi-value register, we want to abstract away from details concerning communication and process structure. Following Burckhardt et al. [START_REF] Burckhardt | Replicated data types: Specification, verification, optimality[END_REF], we model the execution of a weakly consistent system as an abstract execution. An abstract execution A consists of a set of events E and a visibility relation vis ⊆ E × E. The set E denotes the events representing the execution of operations on different nodes of the distributed weakly consistent system. The events have a unique identity and carry the metadata about the object and operation executed on it as well as information relevant for the specific use case (e.g. the subject executing the operation). The vis relation models the dependency between events. For two events e 1 and e 2 , if (e 1 , e 2 ) ∈ vis, then e 1 can influence the effect of e 2 . The local order of events for each process is usually included in the visibility relation. To capture causality, vis must be irreflexive, transitive and antisymmetric. This corresponds to causal visibility. In addition, the visibility relation needs to be well-founded, so we can talk about the next events in the execution. The relation can also be depicted in an event graph where the nodes of the graph are the events and the edges represent the visibility relation. Transitive edges are left out for readability.

We annotate the nodes of event graphs with operation expressions as follows: op(p 1 , . . . , p n ) describes that an event e represents an execution of operation op with parameters p 1 to p n . If the returned value is relevant, we denote it as op(p 1 , . . . , p n ) ⇒ retval where op(p 1 , . . . , p n ) is defined as above and retval represents the returned value. In form of an event graph, the example for the multi-value register can be depicted as in Figure 1. Event e 1 corresponds to an initial put operation, which assigns the single value 0. The put(1) operation of e 2 happens concurrently with another operation, put(2) of e 3 , that also modifies the state of the register. Both events are visible to event e 5 associated to the get operation which yields the set {1, 2} as result. As the example shows, this abstract execution is only concerned with the partial order of events with respect to the visibility relation; the event graph abstracts away from the details of a specific implementation (e.g. which process executes an operation or how operations are distributed to the other process).

The paper makes the following contributions: 1) We show why current temporal logics are not suitable to specify the intended behavior of weakly consistent systems. 2) Our temporal logic called event-based parallel temporal logic (EPTL) based on an abstract execution of the system allows to express properties on the global partial order of the events of the system and takes into account the nonserializability of operations. 3) We have proven laws that allow to rewrite EPTL formulas while retaining the semantics. EPTL is modeled in Isabelle/HOL and all laws are formally verified.

Event-based parallel temporal logic (EPTL)

In this section we present a new variant of temporal logic, namely event-based parallel temporal logic (EPTL).

Why LTL and CTL are not suitable Traditionally, linear time logic [START_REF] Pnueli | The temporal logic of programs[END_REF] (LTL) is interpreted on Kripke structures representing the reachable states of the system. This has two implications: (1) Time is usually seen as linear thereby totally ordering the events of the system and (2) LTL formulas specify properties of the states of the system, not the events. The leads to problems when trying to use LTL to specify properties of weakly consistent systems.

If we regard the serializations of abstract executions like the one in Figure 1 as independent event graphs, none of the executions would yield a result for a get operation that consists of more than one value since no operation would happen concurrently. We would need to encode the temporal information of the original abstract execution into the possible systems states. But this does not scale well and would typically require knowledge of the implementation of the replicated data type. Since the goal is to have a specification logic for the intended behavior of the system, this approach is not an option.

Computation tree logic [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching time temporal logic[END_REF] (CTL) allows for branching time, which solves parts of the issues discussed before. But in weakly consistent systems, the order of events forms a directed acyclic graph (DAG). Allowing to express that multiple different events can be successor of a single event and taking copies of future events is not an option. We would still loose the information that events can have happened concurrently in the past. The extended version [START_REF] Weber | EPTL -A Temporal Logic for Weakly Consistent Systems[END_REF] includes more details.

Syntax and Semantics Instead of being based on possible states of the system, EPTL is directly based on events following many previous works [START_REF] Alur | Deciding Global Partial-Order Properties[END_REF][START_REF] Diekert | Pure future local temporal logics are expressively complete for mazurkiewicz traces[END_REF][START_REF] Havelund | Testing linear temporal logic formulae on finite execution traces[END_REF][START_REF] Thiagarajan | An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces[END_REF]. For an abstract execution A = (E, vis), we define the partial order e 1 ≤ A e 2 ≡ e 1 = e 2 ∨ (e 1 , e 2 ) ∈ vis. When A is clear from the context, we simply write e 1 ≤ e 2 . The satisfaction relation ( A, e) |= ϕ is defined recursively over the structure of the formula as follows: An interpretation I assigns values to all free variables occurring in an EPTL formula. Q[I] stands for the proposition Q in which all free variables are replaced by their interpretation according to I. An EPTL formula ϕ is said to be valid if ( A, e) |= ϕ for all interpretations I. An abstract execution A satisfies an EPTL property ϕ, A |= ϕ, if all starting events of the abstract execution satisfy ϕ. The starting events of an abstract execution A are all events that are minimal with respect to the partial order ≤ A i.e. they have no predecessor events.

( A, e) |= Q iff Q[I](e)
The logical operators ∧ and ⇒ and the remaining temporal logic operators can be defined as usual. The main difference to LTL is that we have two different step operators E X and AX and a different semantics for the until operator U which is tailored to weakly consistent systems. Because the events in the system are ordered using a partial order, the next step is no longer unambiguous. Because of branches of concurrent events, a step might address multiple subsequent events. We want to have the possibility to address either at least one (E X) or all (AX) events that happen immediately after the current event. Also, the semantics of the until operator U has to be adapted to the partial order.

The definition of the until operation is stronger than in previous work [START_REF] Alur | Deciding Global Partial-Order Properties[END_REF][START_REF] Diekert | Pure future local temporal logics are expressively complete for mazurkiewicz traces[END_REF][START_REF] Thiagarajan | An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces[END_REF] to be able to express strong properties about weakly consistent systems like the correctness of access control. Since this is a safety-critical question, we need a specification that is easy to understand and at the same time has a strong semantics on the execution of such a weakly consistent application. In general, access control is about specifying which operations are permitted to be executed by some subject or user on some object in the system. In a simple access control system we consider three types of operations: grant(op, s, o) gives subject s the right to perform operation op on object o. revoke(op, s, o) takes away the right of subject s to perform operation op on object o. exec(op, s, o) represents the execution of operation op performed by subject s on object o. Corresponding propositions (e.g. grant P (op, s, o)) are true for an event e if e represents the execution of the corresponding operation with the given parameters (e.g. grant(op, s, o)).

Based on the given operations, we can define the properties we require from our simple access control system. We want to start with a default policy that initially no user has the right to execute any operation on the system until an administrative user grants this right to him/her. To simplify the example, we do not consider the details of rights to perform grant and revoke operations and assume that there is some administrative user in the system that has the right to perform these operations. Using the weak version of until defined as ( A, e) |= ϕ W ψ iff ( A, e) |= Gϕ ∨ (ϕ U ψ), we can define the initial policy by the following property:

A |= ¬exec P (op, s, o) W grant P (op, s, o)
The dependency between grant and revoke should work like this: Whenever the right of a subject is revoked, this operation should not be executed until a subsequent grant allows the operation again. This can be specified in EPTL in the following way:

A |= G(revoke P (op, s, o) ⇒ AX (¬exec P (op, s, o) W grant P (op, s, o)))

This property both models the semantics of the revoke and grant operations. A grant operation allows an operation that was previously revoked and a subsequent revoke operation disables the operation for the specified user again.

We see that the specifications are both readable and understandable as well as short. The strong semantics of the until operator ensures that revoking the right of a user disallows the operation on all future concurrent paths in the event graph.

Laws Most of the laws of LTL can be shown to also hold in EPTL. Some implications like the distributivity of the conjunction and disjunction are only one-directional. The most important exception to the LTL laws is the induction formula for the until operator, which does not hold in EPTL.

ϕ U ψ ψ ∨ (ϕ ∧ X (ϕ U ψ))
This makes reasoning in EPTL inconvenient. But since EPTL is mainly intended as a specification logic for the intended behavior of the system which translates to properties on abstract executions, this restriction is not a big issue.

Proofs and Extended Version

We have modeled EPTL in the theorem prover Isabelle/HOL. All laws of EPTL are formalized and verified in the interactive theorem prover and are used by the tool to simplify formulas. Even though we did not yet find an efficient automatic checking procedure for EPTL, the proofs can be done in semi-automatic fashion in HOL. Together with the strong automation of Isabelle/HOL this should make for a comfortable environment in which to show that the presented model is suitable to implement access control.

An extended version of this paper [START_REF] Weber | EPTL -A Temporal Logic for Weakly Consistent Systems[END_REF] includes the proven laws and extended examples.

Related Work

Alur et al. [START_REF] Alur | Deciding Global Partial-Order Properties[END_REF] presented a global partial order logic called ISTL. Same as we, they do not restrict the view on the system to the state sequence observed by a local process. The logic is based on a partially ordered set of local states which can also be seen as a branching structure. This branching structure represents all possible sequences of global states that may be derived from the partial order. This state based approach makes it unsuitable for reasoning about weakly consistent systems. As described in Section 2, encoding the events and the conflict resolution strategy into a state requires knowledge about the implementation of the conflict resolution strategy. Since the concrete implementation has to be abstracted from in the specification of the behavior of a weakly consistent system, ISTL is not suitable as a specification language for weakly consistent systems.

The other line of research about partial order semantics uses Mazurkiewicz traces [START_REF] Mazurkiewicz | Concurrent Program Schemes and their Interpretations[END_REF]. The base for these traces is a finite set of actions, which can be seen as state transformations of resources of the system under investigation. Two actions are independent if they act on disjoint set of resources. Only independent actions are allowed to be performed concurrently. This restriction is the reason why Mazurkiewicz traces cannot be used to reason about weakly consistent systems in the given form. In these considered systems, the resources are replicated objects where each process performs operations on its copy. When looking at these operation from a global view, they all change the same shared object. In this sense, the operations are not independent, even though they are possibly performed concurrently. It is not obvious how to apply Mazurkiewicz traces to weakly consistent systems.

Conclusion

We presented the new temporal logic EPTL that is tailored to specify properties of weakly consistent systems. As the example of access control shows, it allows for a concise and readable, yet machine-checkable specification. The complete logic is modeled in Isabelle/HOL and all laws are verified using the theorem prover. All theory files are available under https://softech-git.informatik. uni-kl.de/mweber/EPTL/tree/master.

Fig. 1 .

 1 Fig. 1. Event graph of a multi-value register.

  for variable interpretation I ( A, e) |= ¬ϕ iff ( A, e) |= ϕ ( A, e) |= (ϕ 1 ∨ ϕ 2 ) iff ( A, e) |= ϕ 1 or ( A, e) |= ϕ 2 ( A, e) |= E X ϕ iff ∃e 1 .e < e 1 and e 1 is a minimum wrt < and ( A, e 1 ) |= ϕ ( A, e) |= AX ϕ iff ∀e 1 .e < e 1 if e 1 is a minimum wrt <, then ( A, e 1 ) |= ϕ ( A, e) |= (ϕ U ψ) iff ∃e 1 .e ≤ e 1 such that ( A, e 1 ) |= ψ) and ∀e 3 .e ≤ e 3 such that ( A, e 3 ) |= ϕ exists e 2 such that e ≤ e 2 and e 2 ≤ e 3 and ( A, e 2 ) |= ψ


Alasdair Armstrong

Brijesh Dongol

Modularising Opacity Verification for Hybrid Transactional Memory

Transactional memory (TM) manages thread synchronisation to provide an illusion of atomicity for arbitrary blocks of code. There are various implementations of TM, including hardware (HTM) and software (STM). HTMs provide high performance, but are inherently limited by hardware restrictions; STMs avoid these limitations but suffer from unpredictable performance. To solve these problems, hybrid TM (HyTM) algorithms have been introduced which provide reliable software fallback mechanisms for hardware transactions. The key safety property for TM is opacity, however a naive combination of an opaque STM and an opaque HTM does not necessarily result in an opaque HyTM. Therefore, HyTM algorithms must be specially designed to satisfy opacity. In this paper we introduce a modular method for verifying opacity of HyTM implementations. Our method provides conditions under which opacity proofs of HTM and STM components can be combined into a single proof of an overall hybrid algorithm. The proof method has been fully mechanised in Isabelle, and used to verify a novel hybrid version of a transactional mutex lock.

Introduction

By allowing programmers to mark blocks of arbitrary code as transactions, Transactional Memory (TM) aims to provide an easy-to-use synchronisation mechanism for concurrent access to shared data. Unlike coarse-grained locking, TM implementations are fine-grained, which improves performance. In recent years, TM has appeared as software libraries in languages such as Java, Clojure, Haskell and C++11, and received hardware support in processors (e.g., Intel's TSX).

Software Transactional Memory (STM), as provided by the aforementioned software libraries, offers a programmer-friendly mechanism for shared-variable concurrency. However, it suffers from unpredictable performance which makes it unsuitable for some applications. On the other hand, Hardware Transactional Memory (HTM), as implemented in modern Intel processors, offers high performance but comes with many limitations imposed by the constraints of the hardware itself. For example, HTM implementations do not guarantee progress for a transaction even in the absence of other concurrent transactions [START_REF]Intel: Intel 64 and IA-32 Architectures Software Developers Manual[END_REF]. Hybrid TM (HyTM) implementations address these issues by integrating STM and HTM [START_REF] Harris | Transactional Memory, 2nd edition[END_REF]. Recent work [START_REF] Dalessandro | Hybrid NOrec: A case study in the effectiveness of best effort hardware transactional memory[END_REF][START_REF] Calciu | Invyswell: A hybrid transactional memory for haswell's restricted transactional memory[END_REF][START_REF] Matveev | Reduced hardware norec: A safe and scalable hybrid transactional memory[END_REF] has focused on providing software fallbacks for HTM, combining the performance benefits of HTM with the strong semantics and progress guarantees of STM.

Opacity [START_REF] Guerraoui | On the correctness of transactional memory[END_REF][START_REF] Guerraoui | Principles of Transactional Memory[END_REF] is the primary safety property for TM, which ensures that implementations have the familiar properties of database transactions: atomicity, consistency, and isolation. Opacity requires that all transactions (including aborting ones) can be serialised into some meaningful sequential order, so that no transaction witnesses an inconsistent state caused by the partial execution of any other transaction. Overall, this ensures that TM implementations execute with an illusion of atomicity.

HyTM algorithms, which are the focus of this paper, consist of STM (slow-path) transactions executing in parallel with HTM (fast-path) transactions. Since an execution may consist of only STM or only HTM transactions, one must ensure that slowpath and fast-path transactions are by themselves opaque. In addition, synchronisation between slow-and fast-path transactions must be introduced to ensure that executions consisting of arbitrary combinations of these transactions is opaque. It is already known that naively combining STM and HTM results in a non-opaque HyTM algorithm [START_REF] Calciu | Invyswell: A hybrid transactional memory for haswell's restricted transactional memory[END_REF]. In this paper, we develop a modular verification method for proving opacity of HyTM algorithms-our method provides a means for independently proving opacity of both the STM slow path and the HTM fast path, and then combining them into a proof of opacity of the overall system.

To demonstrate our proof method, in Section 2, we develop a novel hybrid version of Dalessandro et al.'s Transactional Mutex Lock [START_REF] Dalessandro | Transactional mutex locks[END_REF], extending it with a subscription mechanism described in [START_REF] Dalessandro | Hybrid NOrec: A case study in the effectiveness of best effort hardware transactional memory[END_REF]. Our algorithm, HyTML, combines an eager STM, where writes to the shared store are immediately committed to memory, with a lazy fast path HTM, where writes to the shared store are cached until the HTM executes a commit operation. Moreover, it improves concurrency in the original TML algorithm by allowing multiple concurrent writing HTM transactions; in the original algorithm, all transactions abort in the presence of any concurrent writing transaction.

Our proof method is an extension of previous work [START_REF] Lesani | A framework for formally verifying software transactional memory algorithms[END_REF][START_REF] Doherty | Proving opacity of a pessimistic STM[END_REF] that uses trace refinement of I/O automata (IOA) [START_REF] Lynch | Hierarchical correctness proofs for distributed algorithms[END_REF] to verify opacity via a TM specification known as TMS2 [START_REF] Doherty | Towards formally specifying and verifying transactional memory[END_REF]. Unlike existing work, our methods enable one to verify HyTML in a modular manner (i.e., by combining individual opacity proofs of the fast-path and slow-path components) despite the monolithic structure of the algorithm. Our proof methods are influenced by compositional techniques [START_REF] De Roever | Concurrency Verification: Introduction to Compositional and Noncompositional Methods[END_REF] such as rely/guarantee [START_REF] Jones | Tentative steps toward a development method for interfering programs[END_REF]. However, unlike rely-guarantee, which focusses on composing processes, we focus on composition at the level of components, which themselves consist of multiple parallel processes.

We start by developing the notion of an interference automaton (Section 4), which specialises IOA by including transitions that take into account any potential interference from the environment. Parallel composition for interference automata is developed in Section 5, and the notion of weak simulation for parallel interference automata is given in Section 6. There we provide our main decomposition theorem, which describes how weak simulations can be combined to ensure trace refinement of the composed system. We apply our proof methods to verify HyTML in Section 7; we show how individual opacity proofs for the STM and HTM components can be combined, to avoid the complexity inherent in a monolithic proof. All the proofs in this paper, including our meta-theory, have been mechanised 1 in the Isabelle theorem prover [START_REF] Paulson | Isabelle -A Generic Theorem Prover (with a contribution[END_REF]. 1 The Isabelle files may be downloaded from [START_REF] Armstrong | Isabelle files for modularising opacity verification for hybrid transactional memory[END_REF]. [START_REF] Dalessandro | Transactional mutex locks[END_REF] with a 2-counter subscription mechanism [START_REF] Dalessandro | Hybrid NOrec: A case study in the effectiveness of best effort hardware transactional memory[END_REF]. HyTML synchronises the software slow path with a hardware fast path using glb (which is published by software and subscribed by hardware) and ctr (which is published by hardware and subscribed by software).

The parity of glb indicates whether a writing software transaction is currently executing. Namely, a writing software transaction increments glb once at Line 31, where it effectively acquires the write lock, and again at Line 37, where it effectively releases the write lock. Thus, glb/2 gives the total number of committed software transactions. TML, and by extension HyTML, has the property that only a single software transaction can be writing at a time. The presence of a software writer causes all concurrently executing transactions, including fast-path transactions, to abort. 2 . Unlike TML, HyTML allows more than one concurrent writing transaction via the fast path. Variable ctr is used to signal a completed hardware transaction and is incremented whenever a writing hardware transaction commits (Line 16). The total number of committed writing transactions is therefore given by glb/2 + ctr . Note that read-only transactions modify neither glb nor ctr . Software Slow Path. The software slow path implementation is a conservative extension to the original TML algorithm [START_REF] Dalessandro | Transactional mutex locks[END_REF] -we refer the interested reader to [START_REF] Dalessandro | Transactional mutex locks[END_REF][START_REF] Derrick | Verifying opacity of a transactional mutex lock[END_REF] for further details of the behaviour of TML. The implementation consists of operations SPBegin and SPCommit that start and end software transactions, respectively, as well as SPRead and SPWrite that perform (software) transactional reads and writes, respectively. Each operation and transaction-local variable is indexed by a transaction identifier t.

Procedure SPBegin t repeatedly polls both glb and ctr , storing their values in local variables loc t and lctr t , respectively, until loc t is even. This ensures that a software transaction cannot begin until there are no software writers. Procedure SPRead t (a) first reads the value in address a from memory and then checks (non-atomically) if glb and ctr are consistent with loc t and lctr t , respectively. The value of the address is returned if both checks succeed, otherwise it is likely that the transaction t has witnessed an inconsistent snapshot of the store, and hence it aborts.

Procedure SPWrite t first checks the parity of loc t . If loc t is odd, then t must itself be the (unique) software writer, i.e., t had acquired the mutex lock from a previous call to SPWrite t . Therefore, t can immediately proceed and eagerly update the value of * a in the store to v. If loc t is even, it contends with other writers to acquire the lock using a double compare single swap operation: dccs, which atomically checks both lctr t and loc t against their global values and updates glb to loc t + 1 if both are unmodified (which effectively acquires the mutex lock). The dccs operation returns true iff it is successful. If either glb or ctr have changed since t first read their values within SPBegin t , then t may go on to construct an inconsistent memory state, and hence, it must abort. Otherwise (i.e., if dccs succeeds), loc t is incremented (Line 33) to match the new value of glb. This makes the value of loc t odd, allowing the expensive dccs operation to be elided in future calls to SPWrite t , as explained above, and allows future calls to SPRead t to succeed. Procedure SPCommit t always succeeds. It checks to see if t is a writing transaction (i.e., loc t is odd). If so, loc t must be equal to glb, and hence, the update to glb at Line 37 is equivalent to an increment of glb that makes glb's value even. This second increment effectively releases the mutex lock.

Hardware Fast Path. Our implementation uses HTM primitives provided by an Intel x86 processor with TSX extensions. However, we keep the specifics of the hardware generic and assume as little as possible about the behaviour of the primitives, allowing our work to more easily be adapted to work with other HTMs. We use three basic primitives: XBegin, which starts a hardware transaction, XEnd, which ends (and attempts to commit) the hardware transaction, and XAbort, which explicitly aborts the hardware transaction. We assume that, once started, a hardware transaction may be forced abort at any time for any reason, which is consistent with Intel's specifications [START_REF]Intel: Intel 64 and IA-32 Architectures Software Developers Manual[END_REF]. In addition, when interference on any variable that has been read is detected, a fast-path transaction must abort (details are provided below).

Procedure FPBegin t starts a fast-path transaction by calling XBegin, then subscribes to the software global version number, glb, by reading and recording its value in a local variable loc t . A local flag writer t (initially false) is used to indicate whether a fast-path transaction is a writer. Transaction t only begins if loc t is even-if loc t is odd, a slow-path writer is executing, and hence, the fast-path transaction aborts.

Note that because the read of glb occurs after XBegin, the underlying HTM will track the value of glb in memory, ensuring that the fast-path transaction aborts if glb changes. Such checks to glb are performed automatically by the HTM outside the control of the fast-path implementation, and hence, is not explicit in the code (Listing 1). This behaviour is captured in our model of the fast-path transactions by validating that the value of glb is equal to loc t for every step of fast-path transaction t, and aborting whenever this validation fails.

The fast-path read and write operations, FPRead t and FPWrite t consist of standard memory operations, but the underlying HTM will ensures these writes are not visible outside t until t commits. In FPWrite t , the flag writer t is set to true to indicate that t is now a writer. Procedure FPCommit t updates ctr if t is a writer, which indicates to software transactions that a fast-path transaction is committing. Note that this increment to ctr will not cause other fast-path transactions to abort. Finally, FPCommit t calls XEnd, which, for a writer transaction, commits all the pending writes to the store and publishes the increment to ctr.

The TMS2 specification

The basic principle behind the definition of opacity (and other similar definitions) compares a given concurrent history of transactional operations against a sequential one. Opacity requires it be possible for transactions to be serialised so that the real-time order of transactions is preserved. Within this serialisation order, read operations for all transactions, including aborted transactions, must be consistent with the state of the memory store, which is obtained from the initial store by applying the previously committed transactions in their serialised order [START_REF] Guerraoui | On the correctness of transactional memory[END_REF][START_REF] Guerraoui | Principles of Transactional Memory[END_REF]. We elide the formal definition of opacity here, focusing instead on an automata-based TM specification, TMS2 [START_REF] Doherty | Towards formally specifying and verifying transactional memory[END_REF]. Lesani et al [START_REF] Lesani | Putting opacity in its place[END_REF] have mechanically verified that TMS2 is opaque, thus it is sufficient to show trace refinement against TMS2 to verify opacity of an implementation (cf [START_REF] Doherty | Proving opacity of a pessimistic STM[END_REF][START_REF] Lesani | A framework for formally verifying software transactional memory algorithms[END_REF]). TMS2 and the implementations we verify are modelled using input/output automata [START_REF] Lynch | Distributed Algorithms[END_REF][START_REF] Lynch | Hierarchical correctness proofs for distributed algorithms[END_REF]. Definition 1. An I/O automaton (IOA) is a labelled transition system A with a set of states states(A), a set of actions acts(A) (partitioned into internal and external actions), a set of start states start(A) ⊆ states(A) and a transition relation trans(A) ⊆ states(A) × acts(A) × states(A) (so that the actions label the transitions).

TMS2 contains external transitions modelling operation invocations and responses, e.g., the invoke and respond actions for a write action are given below, where status t is a transaction-local variable that models control flow. The transition is enabled if all its preconditions, given after the keyword Pre, hold in the current state. State modifications (effects) of a transition are given as assignments after the keyword Eff.

invt(TMWrite(a, v)) Pre: statust = ready Eff: statust := doWrite(a, v) respt(TMWrite) Pre: statust = writeResp Eff: statust := ready TMS2 contains a pair of invocations and responses for begin, read, write and commit operations. In addition, a response is provided for aborting operations: After invoking a write, read, or commit operation, a transaction may execute one of the 'do' actions in Figure 1, which performs the corresponding abstract operation.

DoReadt(a, n) Pre: statust = doRead(a) a ∈ dom(wrSett) ∨ validIdx t(n) Eff: if a ∈ dom(wrSett) then statust := readResp(wrSett(a)) else v := memSeq(n)(a) statust := readResp(v) rdSett := rdSett ⊕ {a → v} DoWritet(a, v) Pre: statust = doWrite(a, v) Eff: statust := writeResp wrSett := wrSett ⊕ {a → v} DoCommitROt(n) Pre: statust = doCommit dom(wrSett) = ∅ validIdx t(n) Eff: statust := commitResp DoCommitWt Pre: statust = doCommit rdSett ⊆ latestMem Eff: statust := commitResp memSeq := memSeq ⊕ newMemt where maxIdx = max(dom(memSeq)) latestMem = memSeq(maxIdx ) newMemt = {maxIdx + 1 → (latestMem ⊕ wrSett)} validIdx t(n) = beginIdx t ≤ n ≤ maxIdx ∧ rdSett ⊆ memSeq(n)
TMS2 guarantees that transactions satisfy two critical requirements: (R1) all reads and writes of a transaction work with a single consistent memory snapshot that is the result of all previously committed transactions, and (R2) the real-time order of transactions is preserved. Full details of TMS2 may be found in [START_REF] Doherty | Towards formally specifying and verifying transactional memory[END_REF]. Here, we give a brief overview of the requirements that our implementation must satisfy.

To ensure (R1), the state of TMS2 includes memSeq(0), . . . memSeq(maxIdx ) , which is a sequence of all possible memory snapshots (the stores sequence). Initially the sequence consists of one element, the initial memory memSeq(0). Committing writer transactions append a new memory newMem to this sequence (cf. DoCommitW t ), by applying the writes of the transaction to the last element memSeq(maxIdx ). To ensure that the writes of a transaction are not visible to other transactions before committing, TMS2 uses a deferred update semantics: writes are stored locally in the transaction t's write set wrSet t and only published to the shared state when the transaction commits. Note that this does not preclude TM implementations with eager writes, such as TML. However eager implementations must guarantee that writes are not observable until after the writing transaction has committed.

Each transaction t keeps track of all its reads from memory in a read set rdSet t . A read of address a by transaction t checks that either a was previously written by t itself (then branch of DoRead t (a)), or that all values read so far, including a, are from the same memory snapshot n, where beginIdx t ≤ n ≤ maxIdx (predicate validIdx t (n) from the precondition, which must hold in the else branch). In the former case the value of a from wrSet t is returned, and in the latter, the value from memSeq(n) is returned and the read set is updated. The read set of t is also validated when a transaction commits (cf. DoCommitRO t and DoCommitW t ). Note that when committing, a readonly transaction may read from a memory snapshot older than memSeq(maxIdx ), but a writing transaction must ensure that all reads in its read set are from most recent memory (i.e. latestMem memSeq(maxIdx )), since its writes will update the memory sequence with a new snapshot.

To ensure (R2), if a transaction t commits before transaction t then the memory that t reads from must include the writes of t . Thus, when starting a transaction, t saves the current last index of the memory sequence, maxIdx , into a local variable beginIdx t . When t performs a read, the predicate validIdx t (n) ensures that that the snapshot memSeq(n) used has beginIdx t ≤ n, implying that writes of t are included.

Our proof of opacity is based on trace refinement [START_REF] Lynch | Distributed Algorithms[END_REF] between HyTML and TMS2, which ensures that every externally visible execution of HyTML is a possible externally visible execution of TMS2. Since every execution of TMS2 is known to be opaque [START_REF] Lesani | Putting opacity in its place[END_REF], one can conclude that HyTML is itself opaque. We develop a proof method for trace refinement that exploits the fact that HyTML consists of two distinct sets of transactions: slow-and fast-path. Namely, our method proves opacity of each set of transactions independently, taking into account any possible interference from the other set.

Interference automata

In this section, we formalise the concept of interference automata and the notions of trace refinement and forward simulation that we use. Interference automata specialise IOA by explicitly including transitions for environment steps, representing the potential interference from other components within the same system. In the context of the HyTM implementations we verify, an interference automaton will model the fast-path (slowpath) transactions with interference stemming from the slow-path (fast-path).

Definition 2 (Interference automata). An interference automaton A consists of:

-P A is an (infinite) set of process identifiers, The overall state space of A is given by states

-
(A) = (P A → local (A)) × global (A).
That is, a state is a pair consisting of a local state for every possible process in P A and a global state. For any state s, the local part of the state is denoted by s l , and the global part by s g , and hence, s = (s l , s g ).

An interference automaton A may perform an environment transition in env (A), which may only modify the global state, or a local transition for a specific process p ∈ P A , which may only modify the local state of p and the global state. For states s and s , action a, and process p, we denote an internal or external transition of A by s a,p --→ A s , where the action is paired with the process identifier executing the action. By construction, we have that the local state of process p is unchanged after a transition of process p whenever p = p . For global state s g , s g , we use s g -→ A s g to denote an environment transition, which is lifted to the level of states in the obvious way. Namely, if s l is a local state, we let (s l , s g ) -→ A (s l , s g ) denote an environment transition. A run of an interference automaton A is an alternating sequence of states and actions starting from an initial state. The traces of A, denoted traces(A), are the runs of A restricted to external actions, and the reachable states of A, denoted reach(A), are states that can be reached by some run of A. For interference automata A and C, we say C is a trace refinement of A iff traces(C) ⊆ traces(A).

Interference automata may be regarded as a special case of IOA, where the state is specialised and actions are split into internal and environment actions. Therefore, all theorems of IOA, including notions of simulation [START_REF] Lynch | Distributed Algorithms[END_REF] are also applicable in this setting. Note that an interference automaton A represents the actions of an arbitrary amount of processes, which is why P A must be infinite. As such, interference automata represent systems of processes and not specific sets of processes. A forward simulation is a standard way of verifying trace refinement between a concrete implementation and an abstract specification. For interference automata, this involves proving simulation between the external, internal, and environment steps. Definition 3 (Forward simulation). If A and C are interference automata such that external (C) ⊆ external (A), we say R ⊆ states(C) × states(A) is a forward simulation between A and C iff each of the following hold:

Initialisation. ∀cs ∈ start(C) • ∃as ∈ start(A) • (cs, as) ∈ R External step correspondence ∀cs ∈ reach(C), as ∈ reach(A), a ∈ external (C), p ∈ P C , cs ∈ states(C) • (cs, as) ∈ R ∧ cs a,p --→ C cs =⇒ ∃as ∈ states(A) • (cs , as ) ∈ R ∧ as a,p --→ A as , Internal step correspondence ∀cs ∈ reach(C), as ∈ reach(A), a ∈ internal (C), p ∈ P C , cs ∈ states(C) • (cs, as) ∈ R ∧ cs a,p --→ C cs =⇒ (cs , as) ∈ R ∨ ∃as ∈ states(A), a ∈ internal (A) • (cs , as ) ∈ R ∧ as a ,p --→ A as , Environment step correspondence ∀cs ∈ reach(C), as ∈ reach(A), cs g ∈ global (C) • (cs, as) ∈ R ∧ cs g - → C cs g =⇒ ∃as g ∈ global (A) • ((cs l , cs g ), (as l , as g )) ∈ R ∧ as g - → A as g .
Soundness of the forward simulation rule with respect to trace refinement has been checked in Isabelle [START_REF] Armstrong | Isabelle files for modularising opacity verification for hybrid transactional memory[END_REF].

Theorem 1 (Soundness). If R is a forward simulation between interference automata A and C, then C is a trace refinement of A, i.e., traces(C) ⊆ traces(A).

In Section 5, we introduce the concept of parallel interference automata and in Section 6, we develop a theorem for decomposing parallel interference automata into proofs of individual sub-components. It turns out that our decomposition theorem only needs assume the existence of weak forward simulation of the components, in which environment step correspondence may not hold. The notion of a weak simulation is important here, as weak simulations correspond to our existing proofs of opacity for e.g. TML, since these proofs do not involve environment steps. As such, this facilitates the re-use of existing proofs of STM components in the parallel case with only minor modifications. Note that weak simulation between A and C ensures trace refinement for any automaton C in which env(C) is the identity relation since the environment step correspondence proof is trivial.

Parallel interference automata

In this section, we define a notion of parallel composition for interference automata. The idea is that any possible interference from one component of the parallel composition is reflected as an environment transition in the other. Thus, the parallel composition B C comprises an interleaving of the local (internal and external) actions of both B and C.

Two interference automata B and C can be composed iff they are compatible, which only requires that they share the same start state, i.e., gstart(B) = gstart(C). We let denote disjoint union with injections (or inclusion maps) ι 1 and ι 2 .

Definition 4 (Parallel composition). The parallel composition of two compatible interference automata B and C is constructed as follows:

-local (B C) = local (B) local (C), -global (B C) = global (B) ∪ global (C), -P B C = P B P C , -lstart(B C) = {f ∪ g • f ∈ lstart(B) ∧ g ∈ lstart(C)}, -gstart(B C) = gstart(B) = gstart(C) as B and C are compatible, -internal (B C) = internal (B) internal (C), -((ι n (s), g), ι n (a), (ι n (s ), g )) ∈ ltrans(B C) iff ((s, g), a, (s , g )) ∈ ltrans(B)
when n = 1 and ((s, g), a, (s , g )) ∈ ltrans(C) when n = 2, and env (A) = Id , where Id is the identity relation.

Essentially this construction splits both the processes and the internal state space of the automaton into left and right processes and states, respectively. An invariant of any composed automaton is that left processes always act on left internal states, and vice versa. For the parallel composition B C, we typically refer to the automaton B as the left automaton and C as the right automaton. We use L to denote the projection function that takes a combined state of B C and projects just to the part from the left automata B, and similarly for R and C.

Henceforth, we make the environment transitions of interference automata explicit. We introduce the notation I A for an interference automaton A where the environment is the relation I, i.e. env (I A) = I. We write A when env(A) = Id and refer to such A as an interference-free automaton. Note that we therefore have Id A = A.

In Definition 4, the environment of the composed interference automaton (I C B) (I B C) is set to be the identity relation Id , which is possible under the assumption that the local transitions of I C B imply the environment transitions of C (namely I B ), and vice versa. To use this assumption in our proofs, we introduce the notion of a guarantee condition (inspired by rely/guarantee reasoning [START_REF] Jones | Tentative steps toward a development method for interfering programs[END_REF]). We say that an automaton I B guarantees a relation J when

∀s ∈ reach(I B), a ∈ actions(I B), p ∈ P B • s a,p --→ I B s =⇒ (s g , s g ) ∈ J.
This states that every reachable transition in I B modifies the global state only as permitted by J. In other words, if I C B guarantees I B and I B C guarantees I C , then this ensures that every local transition of I C B can be matched with a environment step of I B C, and vice versa.

As mentioned an (interference-free) interference automaton A represents the actions of zero or more transactions of type A. Similarly the parallel composition A A also represents zero or more transactions of type A, with some labelled as from the left A and others from the right. In other words, parallel composition is idempotent for interference free interference automata. This can be shown via a re-labelling of process identifiers, and has been verified in Isabelle (see [START_REF] Armstrong | Isabelle files for modularising opacity verification for hybrid transactional memory[END_REF]).

Theorem 2. traces(A A) = traces(A)

We will use this theorem in the proof of HyTML to split the interference-free IOA specification TMS2 into the parallel composition of two TMS2 components. Thus, to show that HyTML is a trace refinement of TMS2, it will be sufficient to show that the software and hardware components individually are refinements of TMS2.

Simulation proofs for parallel interference automata

For modular verification of a parallel interference automaton, we provide a way to build a simulation of a parallel composition from individual weak simulations of the subcomponents. For example, in HyTML we consider the two concrete fast/slow paths, and prove both of them TMS2 independently. By Theorem 2, we have that traces(TMS2) = traces(TMS2 TMS2), and hence, for modular proofs of opacity, it is sufficient to consider abstract specifications of the form A A.

Consider interference automata I C B and I B C, and an abstract interference automaton I A A. Assume we have weak simulations R and S where

I A A weakly simulates I C B
and,

I A A weakly simulates I B C.
We aim to develop conditions such that R S is a full (non-weak) simulation between A A and B C, where

R S = {(s, s ) • (L(s), L(s )) ∈ R ∧ (R(s), R(s )) ∈ S}.
We now describe the weak simulations R and S, including the state projection functions L and R, and their interaction with the non-weak simulation of the whole system. Graphically, we can visualise weak simulations R and S as

π 1 π 2 π 2 and γ 1 γ 1
where the local states of the left (right) automaton I C B (symmetrically I B C) combined with the global state is represented by ( ). Thus, the left (right) simulation R (S) is over ( ). Each state of the parallel automaton B C, denoted , contains both left and right processes, their local states, as well as the shared global state.

For the weak simulations R and S, we must construct a simulation R S of the form:

π 1 γ 1 π 2 γ 1 π 2
where the environment step of R must correspond to the appropriate program step of S, namely γ 1 . However, we cannot prove this without some additional properties, because we do not know how actions of I B C affect R, and similarly for I C B and S. Note that establishing environment step correspondence (which would turn R and S into non-weak forward simulations) would not help. For example, consider R :

π 1 π 2 A π 2
Because we have no way of guaranteeing that the abstract state after A in R is the same as the abstract state after γ 1 in S, we cannot naively construct a parallel forward simulation. Instead we use non-interference conditions which guarantee that C and B do not affect R and S, respectively. In essence, this enables us to 'stitch' together the two simulations R and S into a simulation of the parallel composition. In other words, the simulation relations used in both component proofs are preserved by the effects of both components' actions on the global state.

Definition 5. The condition nonInterferenceLeft(R, S, B, C, A) holds iff

∀c l , c g , a l , a g , π C , π A , p • L(c l , c g ) ∈ reach(B) ∧ L(a l , a g ) ∈ reach(A) ∧ R(c l , c g ) ∈ reach(C) ∧ (R(c l , c g ), R(a l , a g )) ∈ R ∧ (L(c l , c g ), L(a l , a g )) ∈ S ∧ L(c l , c g ) π B ,p ---→ B L(c l , c g ) ∧ L(a l , a g ) π A ,p ---→ A L(a l , a g ) =⇒ (R(c l , c g ), R(a l , a g )) ∈ R.
where π A and π C are corresponding actions. Symmetrically, we define a condition nonInterferenceRight(R, S, B, C, A).

The reason these conditions are needed is that our guarantee conditions talk purely about the state changes caused by the automaton itself, but not about the simulation relations between automata. While these non-interference conditions at first look complicated due to the amount of notation involved, notice that the local state c l and a l does not change between the pre-and post-condition for the simulation relation R. What this means is that we are really showing only that effects contained within the guarantee conditions do not affect the simulation relation, which means that these conditions turn out to be quite straightforward to prove in practice, as will be seen in Section 7.

Attempting to remove these non-interference conditions to make the method fully compositional might not be worthwhile in practice, as doing so would require full (rather than weak) simulations for each of the components. This proves to be difficult, as it requires induction on the amount of interference within the simulation proof of each component, and it would preclude easy re-use of existing opacity proofs for the fast and slow paths.

We can now state our simulation theorem for parallel interference automata. The theorem states that R S can be strengthened to a forward simulation between B C and A A provided R (S) is a weak simulation between B (C) and A, and certain guarantee and non-interference conditions hold. This theorem has been verified in Isabelle [START_REF] Armstrong | Isabelle files for modularising opacity verification for hybrid transactional memory[END_REF]. Then R S is a (non-weak) forward simulation between B C and A A, and hence traces(B C) ⊆ traces(A A).

HyTML Proof and Mechanisation

In this section we discuss the proof of the HyTML algorithm, and its mechanisation in Isabelle. HyTML is equal to SP FP where SP and FP are the software slowpath and hardware fast-path components, respectively. Recall that we wish to prove traces(HyTML) ⊆ traces(TMS2). We prove that TMS2 TMS2 weakly simulates HyTML via Theorem 3, and thus traces(HyTML) ⊆ traces(TMS2 TMS2). By Theorem 2, traces(TMS2) = traces(TMS2 TMS2), and hence the result follows by transitivity of ⊆.

We start by defining environment relations for all the automata involved. The relation for the interference SP receives from FP, I FP is

Id ∪ {(g, g ) • (odd (glb) -→ g = g ) ∧ ctr ≥ ctr ∧ glb = glb ∧ (even(glb) ∧ store = store -→ ctr > ctr )}.
In words, the fast-path guarantees that: (1) If glb is odd, then it will not affect the global state at all. (2) If glb is even, then any change to the store implies ctr increased. (3) Even if the store remained the same, ctr may still increase, and, (4) The fast path never modifies glb (it only subscribes to it).

SP makes a much weaker guarantee to the FP; I SP guarantees that {(g, g ) • ctr = ctr ∧ glb ≥ glb}.

In words, this means that the software only guarantees that it will not change the ctr variable, and that it only ever increments glb.

The interference from other TMS2 components on TMS2 is given by I TMS2 , which simply allows new stores to be added to the stores sequence (see (R1) in Section 3).

The proof that TMS2 TMS2 weakly simulates HyTML is split into several subparts: First, we show weak simulation of both I FP SP and I SP FP against I TMS2 TMS2. The fast-path proof is much simpler than the slow-path, as the hardware transactional memory abstraction performs most of the fine-grained steps of atomically, which greatly simplifies the verification process. Third, we verify the guarantee conditions from Section 4. Fourth, we verify the non-interference properties in Section 4.

Mechanisation. For HyTM implementations we further specialise interference automata to model the components of a hybrid TM implementation. The set of process identifiers become transaction identifiers, and assuming L and V represent the set of all addresses and values, the set of external actions of a transactional automaton A are fixed, and given by:

external T = {Begin I , Begin R , Commit I , Commit R , Abort, Write R } ∪ {Read I (a) | a ∈ L} ∪ {Read R (v) | v ∈ V } ∪ {Write I (a, v) | (a, v) ∈ L × V }
As mentioned in Section 2, we base our implementation of the underlying hardware transactional memory on Intel's TSX extensions. Therefore, we implement transitions for the XBegin, XEnd and XAbort actions within the hardware automaton. We assume that each hardware transaction is equipped with read and write sets representing the values held in the local processors cache. A simple validation predicate which checks if the values in the read and write set match those in main memory models the cache line invalidation used in the actual hardware. While this validation is more fine-grained than what the actual hardware can do (as it works on the level of cache lines), because the fast path automaton can abort non-deterministically at anytime, all the possible behaviour of the hardware is captured and shown to be opaque. Overly coarse-grained validation might force us to abort when the hardware could succeed, so we err on the side of caution. This behaviour should be generic enough to capture the behaviour of any reasonable hardware TM implementation, not just Intel's TSX. In particular, we do not assume that non-transactional reads and writes can occur within hardware transactions.

Proof in Isabelle. For full-details of our proofs, we refer the interested reader to our Isabelle theories. Here, we briefly comment on the complexity of our mechanisation. In Isabelle, formalising and proving the correctness of the TML slow-path required about 2900 lines, while formalising and proving the correctness of the hardware fast-path re-quired around 600 lines. Proving the non-interference and guarantee conditions required only 450 lines; with the non-interference conditions taking 300 lines and the guarantee conditions requiring only around 70 lines. The formalisation of the transactional automata and requisite theorems took around 2000 lines of Isabelle. Although these are not perfect metrics, they show that the majority of the work was in proving that both HyTM paths satisfy TMS2. Once these individual proofs were completed, bringing the proofs together was fairly comparatively straightforward once the necessary theorems had been set up.

Proving that both HyTM paths are TMS2 is fairly mechanical, and involves detailed line-by-line simulations-showing that every possible step preserves the simulation relation even under interference from every other possible step. Our method enabled adapting our existing work verifying software TML and adapting it to the HyTM case. For simulation proofs of this nature, the number of sub-goals grows geometrically with the number of lines in the algorithm, whereas the non-interference conditions only grow linearly in the modular case. However, we believe that both the conceptual benefits of splitting the proof into its logical sub-components, as well as the ability to re-use existing proofs are the main benefits to modularisation.

Our experience with Isabelle for these proofs was very positive. The powerful tools and tactics within Isabelle were very useful for automating many of the cases produced by the simulation rules.

Conclusion

In this paper we have developed a fully mechanised modular proof method for verifying opacity of HyTM algorithms. Verification of opacity has received considerable interest in recent years (see e.g., [START_REF] Lesani | On the Correctness of Transactional Memory Algorithms[END_REF][START_REF] Derrick | Verifying opacity of a transactional mutex lock[END_REF]). We leverage a simulation-based approach against the TMS2 specification [START_REF] Doherty | Towards formally specifying and verifying transactional memory[END_REF] as well as the known result that TMS2 is itself opaque [START_REF] Lesani | Putting opacity in its place[END_REF]. Our method supports adapting existing proofs of opacity (via TMS2) for both the fast-and slow-path into a HyTM system with only minor modifications to such existing proofs.

We develop the novel notion of interference automata, as well as notions of parallel composition and weak simulation for them. These concepts give us a proof method for combining weak simulations on individual interference automata into a single proof of trace refinement for their parallel composition. All of our meta theory has been checked using the Isabelle theorem prover. To show applicability of our methodology in the context of HyTM algorithms, we develop a novel hybrid extension to Dalessandro et al.'s TML [START_REF] Dalessandro | Transactional mutex locks[END_REF], where we apply a 2-counter subscription mechanism [START_REF] Dalessandro | Hybrid NOrec: A case study in the effectiveness of best effort hardware transactional memory[END_REF]. Our new algorithm allows more concurrency than the original TML as it allows parallel hardware writers.

We conjecture the possibility of further optimisations to the algorithm by removing redundant checks on glb and ctr in the slow-path read operation if loc t is odd. It may also be possible to replace the dccs operation by first acquiring a local value of ctr before acquiring the mutex lock glb using a compare and swap and then checking if the local value of ctr is still valid. However, we have chosen to present a conceptually simpler algorithm that nevertheless demonstrates our proof method. There are more complex HyTMs [START_REF] Dalessandro | Hybrid NOrec: A case study in the effectiveness of best effort hardware transactional memory[END_REF][START_REF] Calciu | Invyswell: A hybrid transactional memory for haswell's restricted transactional memory[END_REF][START_REF] Matveev | Reduced hardware norec: A safe and scalable hybrid transactional memory[END_REF], some with more than two types of transactions; we leave verification of these for future work.

Fig. 1 .

 1 Fig. 1. Internal actions of TMS2

  sets local (A) and global (A) of local and global states, sets external (A) and internal (A) of external and internal actions, and an environment action / ∈ external (A) ∪ internal (A). We assume external (A) ∩ internal (A) = ∅, and use actions(A) = external (A) ∪ internal (A) ∪ { } to denote the actions of A. Furthermore: initialisation of A is described by • lstart(A) ⊆ P A → local (A), a set of local start states, and • gstart(A) ∈ global (A), a global start state transitions of A are described by • ltrans(A) ⊆ (local (A) × global (A)) × actions(A) × (local (A) × global (A)), which describes local transitions, and • env (A) ⊆ global (A) × global (A), which is a reflexive relation that describes environment transitions.

Theorem 3 (

 3 Decomposition). For two compatible interference automata B and C, if R is a weak forward simulation between I A A and I C B, and S is a weak forward simulation between I A A and I B C, where -I B C guarantees I c , and I C B guarantees I B , -nonInterferenceRight(R, S, I C B, I B C, I A A), -nonInterferenceLeft(R, S, I C B, I B C, I A A).

There are some exceptions, e.g., a read-only software transaction can successfully commit even in the presence of another writer if no more reads are performed[START_REF] Derrick | Verifying opacity of a transactional mutex lock[END_REF].

Acknowledgements. We thank Simon Doherty for his helpful comments on this work. Funding is provided by EPSRC grant EP/N016661/1.