Description

This is a challenging project that looks at how results from different fields can be combined.

Memory models describe which reorderings are allowed for read and write actions on shared memory, i.e., which optimisations are allowed. Often the behaviour of a memory model is described in terms
of which write actions can be 'seen' by a read action. Compilers typically ensure that optimisations do not impact the behaviour (only the efficiency) of a sequential program. However, for concurrent
programs, optimisations can introduce new program behaviours. Most memory models provide a so-called DRF guarantee to restrict thebehaviours that can be introduced: if a concurrent program is free of data races, its behaviour is sequentially consistent, i.e., it can be considered as the interleaving of the individual actions.

Several memory model specifications exist, for example TSO, PSO (Total and Partial Store Ordering), and RMO (Relaxed Memory Ordering). However, each chip implements its own memory model, and in general they do not follow these standard memory model specifications. Some chips claim to be
TSO-compatible, but for for example the PSO model no known implementation exists. The hardware memory model descriptions are often not very precise, or the behaviour is only described in terms of
so-called litmus tests.

Goal of this project is to investigate whether techniques from automata theory can be adapted to extract formal specifications of a hardware memory model from its implementation automatically. In particular, we are thinking of techniques such as learning and conformance testing. In learning, an oracle sends communicates with an automaton in a systematic way, in order to learn the automaton. Conformance testing is used to systematically check whether an implementation respects a formal model, described as an automaton. These techniques cannot be directly reused, because hardware memory models are typically not described in such automaton formats, but the hope is that some of
the results and algorithms can be adapted, so that we can learn something about the implementation of hardware models.

Steps in the project

• understand memory model specifications (TSO, PSO and RMO) andformal specifications that have been established for e.g. x86 and ARM
• investigate learning and conformance checking algorithms
• see how these algorithms can be adapted to match the memory modelspecifications
• test the algorithms on concrete hardware