Willemien Visser

SCHÖN: DESIGN AS A REFLECTIVE PRACTICE

In this paper, we present Schön's approach to design, as we have described it in The Cognitive Artifacts of Designing (2006). Schön is (if one excepts the design theorist Rittel) the first author after Simon to introduce a new approach to cognitive design theory. Schön formulated his view on design in terms of "reflective activity" and related notions, especially "reflective practice", "reflection-in-action", and "knowing-in-action". We interpret the activities underlying these notions as forms of what situativity authors have qualified as "situated action" and "situated cognition". In "reflection-in-action", "doing and thinking are complementary. Doing extends thinking in the tests, moves, and probes of experimental action, and reflection feeds on doing and its results. Each feeds the other, and each sets boundaries for the other" (Schön, 1983, p. 280). Reflection-in-action is the reflective form of knowing-in-action: It is Schön's assumption that "competent practitioners usually know more than they can say" (Schön, 1983, p. 8): this illustrates the classical, generally applicable difference between "knowing how" and "knowing that". For Schön, design was one of a series of activities in domains that involve reflective practice: City planning, engineering, management, and law, but also education, psychotherapy, and medicine. As he says it, "the designer constructs the design world within which he/she sets the dimensions of his/her problem space, and invents the moves by which he/she attempts to find solutions." (Schön, 1992, p. 11)

Schön: Design as a Reflective Practice

Except for Rittel, Schön is, as far as we know, the first author after Simon to introduce a new approach to cognitive design theory. Another author of early SIT-inspired1 research is Bucciarelli, who has focused, in particular, on collaborative design analysed from a social perspective.

Schön formulated his view on design in terms of "reflective activity" and related notions, especially "reflective practice," "reflection-in-action," and "knowing-in-action." We interpret the activities underlying these notions as forms of what situativity authors have qualified as "situated action" and "situated cognition" [START_REF] Greeno | Situativity and symbols: Response to Vera and Simon[END_REF].

"Reflective activity" may be defined as the "activity by which [people] take work itself as an object of reflection" (Falzon et al., 1997, quoted in Mollo & Falzon, 2004, p. 532). [START_REF] Schön | The reflective practitioner: How professionals think in action[END_REF] writes: When a practitioner reflects in and on his practice, the possible objects of his reflection are as varied as the kinds of phenomena before him and the systems of knowing-in-practice that he brings to them. He may reflect on the tacit norms and appreciations that underlie a judgment, or on the strategies and theories implicit in a pattern of behaviour. He may reflect on the feeling for a situation that has led him to adopt a particular course of action, on the way in which he has framed the problem he is trying to solve, or on the role he has constructed for himself within a larger institutional context. (1983, p. 62) In "reflection-in-action," "doing and thinking are complementary. Doing extends thinking in the tests, moves, and probes of experimental action, and reflection feeds on doing and its results. Each feeds the other, and each sets boundaries for the other" (Schön, 1983, p. 280).

In a presentation of "Donald Alan Schön (1930Schön ( -1997))" in The Encyclopedia of Informal Education, [START_REF] Smith | Donald schon (schön): Learning, reflection and change[END_REF] writes that, even if Schön was "trained as a philosopher,… it was his concern with the development of reflective practice and learning systems within organizations and communities for which he is remembered." In design circles, one generally refers to Schön as the author who, through his proposal of the reflective-practice concept, offered an alternative to the SIP approach defended by Simon in his Sciences of the Artificial [START_REF] Simon | The sciences of the artificial (3rd[END_REF](Simon, /1996).

Schön's research and thoughts on design thus originate from an educational perspective. Schön was an educator. He was Ford Professor Emeritus on Urban Studies and Education, and Senior Lecturer in the Departments of Urban Studies and Planning, and Architecture, at the Massachusetts Institute of Technology, from the early 1970s until his death in 1997 (Pakman, 2000, p. 5). Schön's enterprise is concerned with the way in which "professionals think in action" as "reflective practitioners" [START_REF] Schön | The reflective practitioner: How professionals think in action[END_REF], and with "educating" this reflective practitioner (Schön, 1987a[START_REF] Schön | Educating the reflective practicioner[END_REF].

Relative to the contrast between the "reflection-in-action" that underlies reflective practice, and "school knowledge" (1987a), Schön does not see himself "as saying anything really new at all." He is drawing on "a tradition of reform and criticism which begins with Rousseau and goes on to Pestilotsy and Tolstoy and Dewey and then, as we approach more contemporary times, Alfred Schultz and Lev Vygotsky and Kurt Lewin, Piaget, Wittgenstein and David Hawkins today" (1987a). It is Dewey who introduced the concept of "reflective conversation with the situation" that is the locus of reflection-in-action (see the title of Schön's famous 1992 paper "Designing as reflective conversation with the materials of a design situation").

According to Schön (1987a), reflection-in-action is the "kind of artistry that good teachers in their everyday work often display," whereas school knowledge refers to a "molecular" idea of knowledge, to "the view that what we know is a product," and that "the more general and the more theoretical the knowledge, the higher it is." From the school-knowledge perspective, "it is the business of kids to get it, and of the teachers to see that they get it."

Reflection-in-action is the reflective form of knowing-in-action. It is Schön's assumption at the start of his famous 1983 book, The Reflective Practitioner, that "competent practitioners usually know more than they can say. They exhibit a kind of knowing in practice, most of which is tacit.… Indeed, practitioners themselves often reveal a capacity for reflection on their intuitive knowing in the midst of action and sometimes use this capacity to cope with the unique, uncertain, and conflicted situations of practice" (1983, pp. 8-9).

In order to show the nature of knowing-in-action, Schön (1987a) uses the example of what happens "if you are riding a bicycle, and you begin to fall to the left." People who know riding a bicycle will do the right thing when in situ, but will often give the wrong answer when asked certain questions, in a classroom or anywhere else, outside of a bike-riding situation. An example of such a question out of context, might be: "If you are riding a bicycle, and you begin to fall to the left, then in order not to fall you must turn your wheel to the ___?" This contrast between "[doing] the right thing when in situ" and being unable to answer correctly when not, requires an explanation: "This capacity to do the right thing.… exhibiting the more that we know in what we do by the way in which we do it, is what we mean by knowing-in-action. And this capacity to respond to surprise through improvisation on the spot is what we mean by reflection-in-action. When a teacher turns her attention to giving kids reason to listening what they say, then teaching itself becomes a form of reflection-in action, and we think this formulation helps to describe what it is that constitutes teaching." (Schön, 1992, p. 11).

Even if not taken from a professional situation, this example illustrates the classical, generally applicable difference between "knowing how" and "knowing that" (Ryle, 1949/1973, pp. 28-40 andpassim).

For Schön, design was one of a series of activities in domains that involve reflective practice: City planning, engineering, management, and law, but also education, psychotherapy, and medicine. Architectural design was the first professional domain studied by Schön in order to develop his epistemology of professional practice based on the concepts of reflection-in-action and knowledge-in-action. In his 1983 book, Schön has "collected a sample of vignettes of practice, concentrating on episodes in which a senior practitioner tries to help a junior one learn to do something.… The heart of this study is an analysis of the distinctive structure of reflection-in-action" (pp. 8-9). Indeed, the characteristics of design that Schön presented as general were displayed in the communicative context that he used to collect his observations, that is, educational situations. Focusing on the education of reflective practitioners in the domain of design, Schön's studies examined design students learning with experienced designers [START_REF] Schön | Designing as reflective conversation with the materials of a design situation[END_REF][START_REF] Schön | Kinds of seeing and their functions in designing[END_REF]. These studies have been conducted in "reflective practicums such as the design studio in architecture" (Schön, 1987a).

Adopting ethnographically-inspired or workplace-oriented perspectives [START_REF] Nilsson | Workplace studies revisited[END_REF] in his analysis of particular educational design projects, [START_REF] Schön | The reflective practitioner: How professionals think in action[END_REF] discusses specific situations in detail, in order to reveal the central role of reflection-in-action in professionals' practice. In their reflective conversations with design situations, designers "frame" and "reframe" problems. In such conversations, "the practitioner's effort to solve the reframed problem yields new discoveries which call for new reflection-in-action. The process spirals through stages of appreciation, action, and reappreciation. The unique and uncertain situation comes to be understood through the attempt to change it." "Furthermore, the practitioners' moves also produce unintended changes which give the situation new meanings. The situation talks back, the practitioner listens, and as he appreciates what he hears, he reframes the situation once again" (Schön, 1983, p. 131-132).

In one of his first papers handling specifically with design [START_REF] Schön | Designing: Rules, types and worlds[END_REF], Schön announces that, "in this paper, [he] will treat designing not primarily as a form of 'problem solving,' 'information processing,' or 'search'" (p. 182). Problem solving is generally considered as handling problems as "given," whereas the process of "problem setting" is neglected. Starting with problems as "given," matters of "choice or decision are solved through the selection, from available means, of the one best suited to established ends. But with this emphasis on problem solving, we ignore problem setting, the process by which we define the decision to be made, the ends to be achieved, and the means that may be chosen. In real-world practice, problems do not present themselves to the practitioner as givens. They must be constructed from the materials of problematic situations which are puzzling, troubling, and uncertain" (Schön, 1983, pp. 39-40). "Problem setting is a process in which, interactively, we name the things to which we will attend and frame the context in which we will attend to them" (id., p. 40, the emphasis is ours).

Naming, framing, moving, and evaluating are central in Schön's view of design. As we see later [that is, in The Cognitive Artifacts of Designing], one of the advances of current SIT-inspired research is the operationalisation of these and other notions that are central in reflective practice.

For Schön, his observations and his approach to these observations "should be contrasted with the familiar image of designing as 'search within a problem space'.… The designer constructs the design world within which he/she sets the dimensions of his/her problem space, and invents the moves by which he/she attempts to find solutions" (Schön, 1992, p. 11).

An example of problem setting in architectural design is the following. Problem setting occurs when architects see the project on which they work in a new way: For example, they see a T-form figure as two L-form figures back to back.

Another design characteristic, introduced through an example from architectural design, is the "seeing-moving-seeing" sequence, which is applied iteratively on "design snippets" [START_REF] Schön | Kinds of seeing and their functions in designing[END_REF].

2 It consists of action sequences such as observing a drawing, transforming it, and, observing the result, discover "certain unintended consequences" of the transformation move (p. 139). Architects may indeed have a certain intention in transforming a drawing, but they are generally unaware of all possible consequences of their actions. Their intention is liable to evolve in their conversation with the drawing. Referring to Simon, Schön notices that it is because of our "limited awareness" and our "limited ability to manage complexity" that designing has this "conversational structure of seeing-moving-seeing" (Schön & Wiggins, 1992, p. 143). Schön and Wiggins refer several times to Sciences of the Artificial, in which Simon introduced his idea of human limited informationprocessing capacity into the theory of designing. They emphasise, for example, that people, therefore, "cannot, in advance of making a particular move, consider all the consequences and qualities [they] may eventually consider relevant to its evaluation" (Schön & Wiggins, 1992, p. 143).

Schön thus notices "the remarkable ability of humans to recognize more in the consequences of their moves than they have expected or described ahead of time" (Schön, 1992, p. 7). As pointed out long ago by the urban designer Christopher Alexander, who is also quoted by Schön, "our ability to recognize qualities of a spatial configuration does not depend on our being able to give a symbolic description of the rules on the basis of which we recognize them" (Schön, 1992, p. 137). Analogously, and as noticed by Alexander as well, even if designers are able to make, tacitly, "qualitative judgments," they are not necessarily able to state, that is, to make explicit, the criteria on which they base them (Schön, 1992, p. 138). This observation once again refers to the knowing-in-action as distinguished from reflection-in-action.

"SIT" is the abbreviation of "situativity," an approach to action, not only cognitive action[START_REF] Greeno | Situativity and symbols: Response to Vera and Simon[END_REF], which Schön adopted in his analysis of design in terms of "reflective pratice".

[START_REF] Goldschmidt | The dialectics of sketching[END_REF] sharpens this idea, distinguishing seeing-as and seeing-that, in a "dialectics of sketching."


Jade Alglave

Assia Mahboubi

A Generic Formalised Framework for Reasoning About Weak Memory Models

This paper describes Coq libraries devoted to the semantic of relaxed memory models. These libraries formalise a framework which covers a large class of industrial models. Implementing this framework inside a proof assistant has significantly helped improving its design and crafting the most concise and relevant specifications. Similarly the use of a proof assistant has been instrumental in the study of the semantic of synchronisation primitives, which we illustrate by the formal proof of a barrier placement theorem. We explain the choices we made to re-design our Coq libraries, and in particular what we gained from adopting a small-scale reflection methodology.

Introduction

Although multiprocessors are an industry standard nowadays, programming and reasoning about such systems remains a challenge. Concurrent programs running on modern multiprocessors exhibit subtle behaviours, making them hard to understand and to debug. Indeed, the order in which the read instructions (e.g. loads) and write instructions (e.g. stores) of a given program are actually executed may no longer be intuitive, i.e. may no longer follow the Sequential Consistency (SC) model [START_REF] Lamport | How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor[END_REF]. The SC model ensures that a program behaves as an interleaving of the different instructions involved by the different threads or processors. However, modern multiprocessors (e.g. x86 or Power) allow optimisations such as instruction reordering, store buffering or write atomicity relaxation [START_REF] Adve | Shared Memory Consistency Models: A Tutorial[END_REF], leading to weak memory models, which are no more SC.

To understand the executions a concurrent program leads to, we need to state precisely what are the guarantees provided by a given memory model. In fact, a memory model should define what value a read instruction to a sharedmemory location can read. For some memory models, such as x86 [START_REF]Intel 64 and IA-32 Architectures Software Developer's Manual[END_REF] and Power [1], the vendor documentation is in informal prose, thus ambiguous. Hence we need to formalise these models in precise and rigorous mathematics, as already highlighted by previous work [START_REF] Sarkar | The Semantics of x86-CC Multiprocessor Machine Code[END_REF][START_REF] Burckhardt | Memory Model Safety of Programs[END_REF].

In [START_REF] Alglave | Fences in Weak Memory Models[END_REF], the first author and others proposed a framework for defining and reasoning about a family of memory models, comprising SC, the Sparc hierarchy [START_REF][END_REF]26], i .e. TSO (which is x86's model [START_REF] Owens | A Better x86 Memory Model: x86-TSO[END_REF]), PSO and RMO, Alpha [START_REF]Alpha Architecture Reference Manual[END_REF], and a significant fragment of Power [1]. The goal was to define formally whether a given execution of a concurrent program is valid on one of these models. This framework describes an execution of a program via partial orders over the memory events yielded by the instructions of the program. These partial orders model for example the program order per thread, the communication through memory (e.g. which read reads from which write), and the orderings induced by the memory barriers, which are special instructions provided by architectures to prevent some of the aforementioned optimisations. The validity of an execution boils down to the acyclicity of several combinations of these partial orders. This formalisation is generic, in the sense that it allows to generalise or reuse from one model to another the subtle reasonings required by weak memory models. Thus, as exposed in [START_REF] Alglave | Stability in Weak Memory Models[END_REF], it becomes possible to obtain generic results on the semantics of synchronisation primitives in a program running on a model of this framework, to force this program to behave as if running on SC.

Yet, as in many other areas of program verification, the proofs involved in this formalisation are tedious and intricate, even if they require a relatively small, essentially combinatorics, mathematical background and even if the mathematical content of the proofs is most often uninteresting. We believe the use of a proof assistant to be crucial for managing these investigations, both to craft the most concise specifications of the models and to provide a high guarantee on the correctness of the proofs and the consistency of the framework. The latter has been demonstrated by impressive previous pieces of work in the formalisation of semantics of instruction sets [START_REF] Myreen | Verified LISP implementations on ARM, x86, and PowerPC[END_REF][START_REF] Fox | Specification and verification of ARM hardware and software[END_REF][START_REF] Fox | A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture[END_REF] or compiler issues [START_REF] Leroy | Formal certification of a compiler back-end, or: programming a compiler with a proof assistant[END_REF][START_REF] Sevcik | Relaxedmemory concurrency and verified compilation[END_REF].

In [START_REF] Alglave | Fences in Weak Memory Models[END_REF][START_REF] Alglave | Stability in Weak Memory Models[END_REF], the authors present the theoretical results they have obtained and the testing tool they have developed, mentioning that all these results have been formalised in the Coq [START_REF]The Coq System[END_REF][START_REF] Bertot | Coq'Art[END_REF] system without describing their libraries. In the constructive type theory underlying Coq, the main issue raised by such a formalisation is to find a convenient representation for finite sets and to benefit from a body of formalised theory of boolean binary relations. The formalisation mentioned in [START_REF] Alglave | Fences in Weak Memory Models[END_REF][START_REF] Alglave | Stability in Weak Memory Models[END_REF] is based on the standard library of Coq augmented with the excluded middle axiom. In particular, it relies on the generic library on sets which offers little support for our needs. These naive choices actually revealed inappropriate, and the code is now difficult both to maintain and to extend.

The purpose of this paper is to present our ongoing rewriting of this formalisation, which covers so far the theoretical results described in [START_REF] Alglave | Fences in Weak Memory Models[END_REF]. The design of the code has been improved along two directions: first we stand on a better library on finite sets, second we use a small scale reflection methodology [START_REF] Gonthier | An introduction to small scale reflection in Coq[END_REF], as coined by G. Gonthier after his formalisation of the proof of the Four Colour Theorem. The first issue could have been addressed by choosing a better suited library in the standard distribution of the Coq system. The second point consists in choosing carefully the data-structures of the formalised objects so that proofs can best benefit from the computational abilities of the Coq type theory. We get rid of the excluded middle axiom by adopting boolean specifications, which significantly eases the formalisation.

Since the last aspect had a positive impact on our formalisation, we used the SSReflect extension [START_REF] Gonthier | A small scale reflection extension for the Coq system[END_REF] to the Coq system which provides a set of tactics dedicated to this methodology. We also benefited from the Coq libraries de-veloped by the Mathematical Component project1 , which include in particular a theory of finite sets, finite graphs, and boolean relations. We have extended the material already available in the existing Mathematical Component libraries with some extra results needed for the present work, like a pigeon-hole lemma and the formal correctness proof of a topological sorting procedure.

We first briefly overview in section 2 the data-structures that we adopted. In section 3, we present the formalisation of the main objects of our study: event structures, executions and architectures. In section 4, we show how to encode a memory model in this framework. Section 5 presents the formal proof of the main theorem of [START_REF] Alglave | Fences in Weak Memory Models[END_REF] on barrier placement. In section 6, we conclude by presenting first some related work, then some directions of future work. The old implementation and our ongoing development are available online2 .

Boolean relations, finite sets, pigeon hole arguments

We present here the features of the Mathematical Component library that we rely on in the present work. Thus, most of the material is not new, except the pigeon-hole lemma-suggested by C. Cohen-and the correctness of the topological sorting procedure.

Boolean reflection. In the standard Coq related literature, reflection usually refers to a proof methodology, where a symbolic representation-usually an inductive type-models a fragment of the inhabitants of a given logical type. This symbolic representation then becomes the input of some decision or simplification procedure and enables relatively large scale computations. Most often, this symbolic representation is hidden to the user, and translated back to its logical form once the desired computation has been performed. By contrast, the smallscale reflection [START_REF] Gonthier | An introduction to small scale reflection in Coq[END_REF] leaves the symbolic representations explicit in the definitions and lemmas, and the translations between symbolic and logical worlds should be locally and explicitly performed by the user when needed in the proof.

Boolean reflection is an instance of small-scale reflection, where the bool data type reflects the fragment of the Coq Prop sort on which the excluded middle holds. Thus, any statement whose truth value can be effectively computed should be modeled by a boolean predicate, coerced to the Prop sort. The excluded middle principle on a boolean statement boils down to case analysis on the value of the boolean, and equivalences between boolean statements are boolean equalities. Hence, the simplification of large boolean conjunctions or disjunctions becomes very fluid, whereas it otherwise imposes a tedious splitting and casing bureaucracy. Rewriting becomes prominent in the proof scripts: we replace subparts of the statements by simpler, equivalent, boolean expressions, up to the point they get an explicit value-true or false-then partially evaluate the whole boolean expression.

The current standard tactic language of the Coq system actually provides little support for small scale methodology, specially regarding the pervasive translations between logical and boolean worlds. For this reason, the present development makes use of the SSReflect tactic extension language distributed with the Mathematical Component libraries.

In what follows, (pred T) is the type of boolean unary predicates on the arbitrary type T and (rel T) is the type of boolean binary relations on T. We use the notations provided by the library; for example, [pred x : T | E] denotes the predicate (fun x => E) and [rel x y | E] denotes the relation (fun x y => E). The notation (relU r s) is the union of two relations operating on the same type, and (subrel r s) denotes the (non-boolean) property that the relation r is included in the relation s.

Equality types, finite types, finite sets. We call equality type a type equipped with a boolean comparison operator. This operator, denoted by a generic infix (_ == _) notation, should be proved equivalent to the default structural Prop equality provided by Coq on this type, denoted (_ = _). In this paper, we will in fact only work with data (values, locations, processor indexes,. . . ) modeled by types with a finite, abstract and arbitrary large number of inhabitants, called the size of the universe. The Mathematical Component distribution defines a finite type (T : finType) by the duplicate free enumeration of its inhabitants. A finite ordinal ('I_n : finType), which is the type of natural numbers smaller than n, is a typical example of such finite type. A finite type can be canonically equipped with a structure of equality type. The distributed library provides a comprehensive corpus of operators and formalised theory for these finite types, which we introduce when necessary. Sets of elements on a finite type carrier T have the type {set T} (see [START_REF] Gonthier | An introduction to small scale reflection in Coq[END_REF] for more details).

Finite types benefit constructively from classical logic and choice principles, since comparison and testing boolean properties become effective on such types. Thus, properties arbitrarily quantified on a finite type can be tested, hence modeled by boolean predicates. The notation (forallb x : T, P) denotes the boolean proposition: for all (x : T), the boolean property P holds. The notation (existsb x : T, P) refers to the existential boolean quantifier. The classical lemmas on the negation of quantified formulas become provable, stated as an equality between two boolean values:

Lemma negb_forall (T : finType)(P : pred T) : ~~(forallb x, P x) = (existsb x, ~~P x).

Equivalence lemmas allow to switch back and forth between the boolean quantifiers and the usual logical quantifiers in the Prop sort when possible and needed. When a function (f : aT -> rT) has a finite domain (aT : finType), and an equality type codomain (rT : eqType), its injectivity becomes testable, by checking whether the sequence obtained by mapping f on the enumeration of aT is duplicate-free. In addition, we can exhibit two distinct elements in the domain of f which have the same image when f is not injective. This is the cornerstone of pigeon-hole based arguments, a frequent key point of our proofs (see sections 4 and 5). We have proved formally the following version of pigeon-hole:

Lemma pigeon_hole (T : finType)(f : nat -> T) : {i : nat & {d : nat | i + d <= #|T| & f i = f (i + d.+1)}}.
which we found the most useful generic formulation in our setting. This lemma states that for any function (f : nat -> T) where T is a finite type, it is possible to compute two natural numbers i and d, such that (i + d) is smaller than the number of elements of T and such that (f i = f (i + d + 1). We first prove that the restriction (g : 'I_#|T|.+1 -> T) of f to the natural numbers smaller than (#|T|.+1) cannot be injective, hence the existence of two numbers mapped to the same image. We typically use this lemma to show that for a function ( phi : T -> T) where T is a finite type, the iteration of phi starting from an (x0 : T) is necessarily cyclic. In that case, we apply the pigeon_hole lemma to the function associating a number n with the n-th iteration of phi on x0.

Order extensions

The Mathematical Component libraries also contain libraries on sequences (lists), paths and finite graphs which originate from G. Gonthier's proof of the Four Colour Theorem. Consider an arbitrary equality type T, a relation (e : rel T), an element (x : T) and a sequence (p : seq T). Let [x 0 , . . . , x n ] denote the sequence (x :: p) where x 0 is x and x n is (last x p), the last element of p with default value x. The sequence (x :: p) is by definition a path for the relation e, denoted (path e x p), if (e x i x i+1 ) holds for any i < n. For instance, (traject f x n) is the sequence of length n obtained by successive iterations of the function f starting from x. It is a path for the relation which links a point to its image by f. A sequence p is a cycle for the relation e, denoted (cycle e p), if (path e x (rcons p x)) holds, where (rcons p x) adds x at the end of p.

The Mathematical Component library provides a specific library devoted to boolean relations on a finite type domain, which can be seen as a formalisation of finite graphs. This library provides in particular the construction of the transitive closure (connect e) of a relation (e : rel T), where T is a finite type, by implementing and certifying a depth-first search algorithm (see [START_REF] Gonthier | An introduction to small scale reflection in Coq[END_REF]). Following the same approach, we have implemented the construction of a total acyclic relation from an acyclic relation by implementing a topological sorting algorithm. To do so, we use the choice operator on finite types, which inspects all the elements of the finite type in the order provided by the underlying enumeration: [pick x \in A] (resp. [pick x \in A | P]) is an element in (option T), which is (Some x) if a witness of A (resp. a witness of the boolean predicate P satisfying A) has been found among the elements of T and None otherwise. We define the topological sorting as follows: We define this function recursively on a counter n and the topological sorting is local to the set s. The counter is imposed by the Fixpoint construction of the Coq system, which requires a syntactic termination check. If the counter is non-zero, then the function looks for an element in the set s which has no predecessor by the relation e. If there is no such element, the relation is e itself. If there is a witness x, the relation is the union of the topological sorting of the set (s :\ x) (s where x has been removed), and of the relation which relates x to any element of (s :\ x). Since since one element is removed from the initial set at each recursive call, the complete topological sorting is performed as soon as the counter is equal to or larger than the cardinal of the set s. We prove easily that this relation is always an extension of its argument:

Lemma topo_rec_subrel (e : rel T) (s : {set T}) (n : nat) :

subrel e (topo_rec e s n).

We also prove by induction on the counter that it is asymmetric (resp. transitive) as soon as its argument is asymmetric (resp. transitive) on the input set: where {in s & &, p} means that the binary (non necessarily boolean) predicate p holds when both its arguments are in s. For the last two proofs, we distinguish the set on which the sorting is performed from the set on which the property is transmitted. Thus, we obtain directly an induction hypothesis which is strong enough for the induction on the counter to solve the proof easily. From its asymmetry, we trivially deduce that topological sorting is irreflexive and since it is also transitive, it is acyclic. Finally if the value of the counter is large enough, the output relation is total on its input set as soon as its input relation is acyclic: where the acyclic_on Prop predicate ensures that no sequence of elements in s is a cycle for e, and the strict_total Prop predicate on boolean relations ensures that for any two distinct elements x and y, either (e x y) or (e y x).

For this property, the value of the counter matters, because if the counter is not large enough, the sorting stops at an intermediate state, and there is no reason why the computed relation should be already total. This proof mainly consists in showing that the acyclicity hypothesis ensures the existence of a predecessor-free witness at each recursive call: if every element of the set on which we operate has a predecessor, then we can find a cycle for the relation among the elements of this finite set using the pigeon-hole principle.

We were able to find only one reference which explicitly mentions a formal proof of correctness of a topological sorting [START_REF] Roux | Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence[END_REF], available as part of the Coq CoLoR library [START_REF] Blanqui | CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates[END_REF]. Its computational content is only available through extraction and not as a computable Coq program. However, the underlying algorithm is not realistic, in particular due to repeated calls to a transitive closure process to ensure transitivity: computation was certainly not the motivation of the authors but rather the theoretical existence of the linearisation process. By contrast, we wanted to describe an ideal implementation in Coq of the algorithm, with naive data structures (such as the generic pick), but with a code fairly close to a realistic functional implementation (see section 6). We have however proved the specification of the non-tail recursive version because it was easier to handle in the proof. Proving the equivalence of the above program with its tail recursive counterpart is then a straightforward induction on the counter.

Event structures, executions, architectures

The framework proposed in [START_REF] Alglave | A Shared Memory Poetics[END_REF][START_REF] Alglave | Fences in Weak Memory Models[END_REF] abstracts from the semantic of assembly code instructions by reasoning only about the memory events issued by the instructions of a given program. We first define the finite types Value, Proc, Location, Eiid and poi which are respectively modelling values, a set of unique identifiers for processors, locations, a set of unique identifiers for events and the type of indexes in programs order, as natural numbers bounded by a global constant.

Event structures A memory event (m : Event) is a triple which consists of a unique identifier (e : Eiid), an instruction identifier (i : Iiid) and the action (a : Action) it performs. An instruction identifier consists of a pair of a processor identifier (p : Proc) and the index of its line (l : poi). An action is an access in the memory and is encoded as a triple containing the direction Dirn (read R or write W) of the action, its location and its value: For instance, the event "At the line 1 of the program, the value 2 is read from location x on processor P 0 " uniquely identified by the label 12 is represented by the term: (mkEvent 12 (mkiid 0 1)(Access R x 2)).

Programs are abstracted by event structures. An event structure

E (E, dp →),
is composed of a (finite) set of events E and the dependency (boolean) relation A well-formed execution witness requires its write serialisation to be a perlocation total order on the write events. This models the memory coherence assumed by modern architectures [START_REF]Alpha Architecture Reference Manual[END_REF]1,[START_REF][END_REF]26,[START_REF]Intel 64 and IA-32 Architectures Software Developer's Manual[END_REF], linking a write w to any write w ′ to the same location hitting the memory after w. In addition, the read-from map rf → should link a write w to a read r from the same location that reads from w. We also require that for every read from a given location, there exists a unique write to the same location from which the read takes its value.

Note that until now, all the relations that we defined would also be necessary to describe SC executions. To integrate weak memory models considerations into the picture, we derive an additional relation fr → (for from-read map), from the write serialisation and the read-from map relations, which relates two events e r and e w such that there is a write e w ′ from which e r reads (ie. e w ′ rf → e r ) and e w ′ hits the memory before e w does (ie. e w ′ ws → e w ).

The semantics intuition of fr → is as follows. Some of the weaknesses of memory models arise in our framework because the read events may take their values not only from the main memory, but also from store buffers and caches. This means that we cannot determine at which instant of time the value read by a given read event is actually in the main memory. We can only determine an interval of time in which this value is in the memory, i.e. between the write that wrote this value hit the memory and the next write to the same location in the write serialisation. Thus, the fr → relation allows us to represent this interval, for it relates a given read event to both the write from which it reads its value (via the rf → relation) and the next write to the same location in ws →. →. In a shared-memory multiprocessor, some pairs of instructions in the program order may be reordered. Hence in an event structure e, for two events e 1 and e 2 such that e 1 po → e 2 , we only know that they will happen in this order if the architecture ensures that e 1 ppo → e 2 . TSO for example authorises write-read pairs to be reordered, but nothing else [START_REF][END_REF]26]:

Architectures

ppo → = po → \ (W × R).
On any architecture, in any execution, as soon as e 1 ws → e 2 or e 1 fr → e 2 , we know that the event e 1 happens before event e 2 . However, in most if not all shared-memory multiprocessors, a write may be committed first into a store buffer, then into memory; this optimisation is known as store buffering [START_REF] Adve | Shared Memory Consistency Models: A Tutorial[END_REF]. In some architectures, like PowerPC, a write can be written first to a cache, then to the main memory; in this case we say that the write is not atomic, for this optimisation is known as store atomicity relaxation [START_REF] Adve | Shared Memory Consistency Models: A Tutorial[END_REF]. In practice, these two optimisations mean that while a write transits in store buffers and caches, a processor may read a past value. Hence in an execution x, for two events e 1 and e 2 such that e 1 rf → e 2 , we only know that the event e 1 will happen before e 2 if the architecture ensures that e 1 grf → e 2 . This captures the specification of TSO which authorises store buffering but considers stores to be atomic or the specification of Power which relaxes the atomicity of writes.

Last, architectures provide barrier instructions to order on certain pairs of events. We gather the orderings induced by barriers in the global relation ab → : as soon as e 1 ab → e 2 , we know that the event e 1 happens before event e 2 .

We are now able to define a global happens before relation ghb → . If two events e 1 and e 2 in an execution witness of a given event structure are ordered by e 1 ghb → e 2 , then the architecture ensures that the event e 1 happens before event e 2 . On an architecture A, and an execution X of the event structure E, this relation ghb → is defined as the union of the relations known to be global on A: Definition ghb A E X : rel Event := relU (relU (relU (relU (grf A X) (ab A E X)) (ws_of_EW X)) (fr X))

In our framework, the main validity condition of an execution consists of the acyclicity of the ghb → relation, which means that we can think of an execution as exhibiting a global timeline of certain events from the memory point of view.

Validity We now need to determine when a given execution of an event structure is considered as valid on a given architecture. For this purpose, we first define a relation gathering all the communication arrows between events of an execution: Definition com (X : Execution_witness) : rel Event := relU (relU (rf_of_EW X) (fr X)) (ws_of_EW X).

We need to define also the po-loc → relation, which corresponds to the program order restricted to events that share the same memory location. The uniproc(E, X) acyclic( com → ∪ po-loc → ) condition models the fact that all the values that a given memory location can take on a weak memory model are in fact already accessible on SC 4 . This is how we model the memory coherence property, as widely assumed by the existing architectures [START_REF]Alpha Architecture Reference Manual[END_REF]1,[START_REF][END_REF]26,[START_REF]Intel 64 and IA-32 Architectures Software Developer's Manual[END_REF]. The thin(E, X) acyclic( rf → ∪ dp →) condition prevents executions where values seem to come out of thin air [START_REF] Manson | The Java Memory Model[END_REF]. We only need to add the thin check on our framework so as to embrace Alpha in our framework: for all the other models, because dp → ⊆ ppo → , the thin check is subsumed by the acyclicity check of ghb → [START_REF] Alglave | A Shared Memory Poetics[END_REF]. Finally, an execution (E, X) is valid on an architecture A when the relation A.ghb(E, X) is acyclic, together with the two above checks. We model this in Coq by the following three component conjunction:

Definition valid_execution A E X : Prop := [/\ acyclic (relU (com X) (po_loc E)), acyclic (relU (rf_of_EW X) (dp_of_ES E)) & acyclic (ghb A E X)].
Amongst these three requirements, only the last one actually depends on the architecture. We consider an architecture as a filter over executions, determining whether they are valid or not, whereas the well-formedness check gathers constraints over programs. Hence, since the first two checks model constraints over executions and not on programs, we include them in the execution filter.

The native definition A n of a real-world architecture as exposed in the vendor documentation, never matches the form of an architecture as defined in Sec. 3. Thus, we should check that A n and its encoding A in this framework define the same validity conditions over executions. All the documentations or model descriptions that we studied (i.e. SC, Sun TSO, PSO, RMO, Alpha, Power and x86) share a common style, as exposed below, except Power and x86. The x86 model has been discussed to be a TSO model [START_REF] Owens | A Better x86 Memory Model: x86-TSO[END_REF], thus what follows apply. We discuss the case of Power at the end of this section. We now explain how we model each architecture in a generic style close to the documentation, then how we encode it into the framework presented in section 3.

A common description of native architectures The description of SC [START_REF] Lamport | How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor[END_REF] and the documentations of Sun TSO, PSO, RMO [START_REF][END_REF]26] and Alpha [START_REF]Alpha Architecture Reference Manual[END_REF] all describe an execution as an order ex on events. They define the execution ex to be valid if it is a strict partial order on events which moreover contains a certain (architecture dependant) subrelation of the program order 5 . The relation ex should be understood as our global happens-before relation.

For convenience, and since we proved formally in Sec. 2 that any partial order can be extended to a total order, we describe the native models in terms of a total order. This means that for an execution defined as a partial order, we consider all its linear extensions to be valid native executions.

For a given architecture A n , and an event structure E, we write A n .ppo(E) for the subrelation of the program order distinguished by the architecture. We write A.native(E, ex) when ex satisfies the conditions imposed by A n . The literal formalisation of a vendor documentation is hence of the form:

A.native(E, ex) total-order(ex, evts(E)) ∧ (A n .ppo(E) ⊆ ex))
Equivalence proofs Given a native architecture A n , we want to show that we can build an instance of the framework which defines a validity criterium A.valid on execution witnesses equivalent to the check A.native. This means that whenever an execution ex satisfies A.native, we can build an execution witness (E, X) which is valid on A, such that ex and (E, X) have the same events and the same communication relations ws → and fr →. Conversely, from an execution (E, X) valid on A, we should be able to build an execution ex valid on A n with the same events and communication relations. Formally, we need to build an instance A of the generic framework such that:

∀EX, A.valid(E, X) ⇔ ∃ ex, A.native(E, ex) ∧ wit(ex) = X
where wit(ex) stands for an execution witness built from ex.

Candidate execution witnesses

We now explain how to extract execution witness candidate from the order relation ex, i.e. how to build wit(ex).

For this purpose, we need to extract rf → and ws → from an order ex. We write rf(ex) (resp. ws(ex)) for the rf → (resp. ws →) extracted from ex. We define (x, y) to be in rf(ex) when x is a write and y a read, both to the same location, such that x is a maximal previous write to this location before y in ex, written pw(ex, r). Formally, we have pw(ex, r) {w | loc(w) = loc(r) ∧ w ex r}, writing loc(m) for the location of an event e, and rf(ex) {(w, r) | w = max ex (pw((ex), r))}.

We define (x, y) to be in ws(ex) when x and y are writes to the same location and x ex y. Formally, writing W ℓ for the set of write events to the location ℓ, we have ws(ex) ℓ (W ℓ × W ℓ ) ∩ ex. We derive the from-read map fr(ex) following the definition given in Sec. 3.

Note that the extracted rf → and ws → are well-formed in a finite execution, hence the execution witness wit(ex) = (ws(ex), rf(ex)) is well-formed as well.

From native architectures to the framework At that point, finding a suitable candidate well-formed instance of the generic framework capturing the native architecture causes no difficulty. We simply take A = (A n .ppo, A n .grf, ∅), where A n .grf(ex) returns the fragment of rf(ex) defined to be global by A n . For example, on TSO, the store atomicity relaxation is not allowed, but store buffering is, hence A n .grf(ex) will return the internal rf →, i.e. the fragment of rf(ex) that relates events from the same processor. Now we need to show that, for a given event structure E, we can build an execution X, associated with E and valid on A. It follows from their definition that the extracted read-from maps rf(ex), write serialisation ws(ex) and the extracted from-read maps fr(ex) are included in ex. Moreover, since ex contains A n ppo(E), we know that ex contains the ghb → relation of the extracted execution witness wit(ex). Thus, the acyclicity of ghb → follows from ex being a total order6 : ∀E ex, A.native(E, ex) ⇒ A.valid(E, wit(ex))

From the framework to native architectures This step causes no difficulty as well: the ex relation is the topological sort of the transitive closure of the globalhappens-before ghb → relation provided by the candidate architecture. By wellformedness hypothesis (see section 3) of the execution, ghb → should be acyclic on the events. This acyclicity property is preserved by the transitive closure, which is hence transitive and irreflexive. Hence we can apply the topological sorting construction described in section 2, which results in the appropriate ex.

Implemented models In the original formalisation, we have defined SC, Sun TSO, PSO, RMO and Alpha as instances of our framework and proved in Coq the equivalence of our definitions with the original definitions. The code can be browsed online. At the time of submission, only the SC model has been reimplemented. We plan to add the re-implementation of the other models online during the review process, which should be without difficulty as these formal proofs are rather routine work.

The framework of Sec. 3 embraces a fragment of Power as well. For Power, since no formal definition existed, the first author and others presented in [START_REF] Alglave | Fences in Weak Memory Models[END_REF] an intensive testing experiment against three generations of Power machines. This lead to the design of a fragment of a Power model, given in [START_REF] Alglave | Fences in Weak Memory Models[END_REF], as an instance of the framework presented in Sec. 3.

Semantics of barriers

We now present the formalisation of the main theorem presented in [START_REF] Alglave | Fences in Weak Memory Models[END_REF], which addresses the semantics and placement of memory barriers in a program, to ensure that it only has strong executions, for example SC ones. We say that an architecture A 1 is weaker than an architecture A 2 if A 1 exhibits at least all the behaviors of the stronger one A 2 :

∀A 1 A 2 , (A 1 ≤ A 2 ) (∀EX, A ǫ 2 .valid(E, X) ⇒ A ǫ 1 .valid(E, X))
where A ǫ represents A without barriers, i.e.

ab →= ∅. For instance, the SC model is stronger than any weak architecture we have mentioned so far. Observe that this definition can be implemented as:

A 1 ≤ A 2 ( ppo1 → ⊆ ppo2 → ) ∧ ( grf1 → ⊆ grf2 →
). We now want to study how to simulate the behavior of a strong architecture over a weaker one, by studying the semantic of the barrier instructions. For instance we may want to show that the semantic of barrier instructions, together with a correct placement of these barriers in the code make possible to forbid non-SC executions on a weak architecture. For this purpose, we define the predicate fb (fully barriered ) on A 1 ≤ A 2 as: The fb predicate provides an insight on the strength that the barriers of the architecture A 1 should have to restore the stronger A 2 . They should (i) maintain the pairs preserved in the program order on A 2 and not on A 1 and (ii) compensate for the fact that some writes may not atomic on A 1 while they are on A 2 , which we model by (some subrelation of) rf → not being global on A 1 while it is on A 2 . The main theorem of [START_REF] Alglave | Fences in Weak Memory Models[END_REF] shows that the above condition on ab1 → regains A ǫ 2 from A 1 , a property that we call the barrier guarantee:

A 1 .fb A2 (E, X) ( ppo 2\1 → ) ∪ ( grf 2\1 → ; ppo2 → ) ⊆
∀A 1 A 2 , (A 1 ≤ A 2 ) ⇒ (∀EX, A 1 .valid(E, X) ∧ A 1 .fb A2 (E, X) ⇒ A ǫ 2 .valid(E, X))
The only difficulty of this proof is to show the acyclicity of the global happens before relation of the stronger architecture A 2 under the assumptions of the theorem. We have simplified the argument previously formalised, and described in [START_REF] Alglave | A Shared Memory Poetics[END_REF], to reduce it the (somehow ad-hoc) following acyclicity criterium:

Lemma acyclicity_crit : forall (T : finType)(r1 r2 : rel T), acyclic r1 -> (forall x y z, r2 x y -> r2 y z -> r1 x y || r1 x z) -> acyclic r2.

This lemma is again a simple application of the pigeon-hole principle: if a given sequence is a cycle for the relation r2, then the hypothesis of the criterium ensures that any element in the sequence has a successor by relation r1 among the other elements of the sequence: either its successor in the r2-cycle, or the successor of its successor. Therefore, the pigeon-hole principle ensures the existence of a r1-cycle built from elements in the initial r2-cycle. → e 3 . Finally, the hypotheses of the criterium are satisfied with r1 set at A 1 .ghb(E, X) and r2 set at A ǫ 2 .ghb(E, X), which completes the formal proof of the barrier guarantee.

Related Work and Conclusion

There is extensive related work on the semantics issues associated with memory models. For the sake of brevity, we focus here exclusively on the formalisation of hardware models inside a proof assistant. The work presented in [START_REF] Fox | Specification and verification of ARM hardware and software[END_REF][START_REF] Fox | A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture[END_REF] studies the formalisation of the ARM architecture, with a particular focus on the instruction set. In our context, we abstract away from the instruction semantics via for example the dp → relation, and leave the integration of instruction sets for further work. The work presented in e.g. [START_REF] Sarkar | The Semantics of x86-CC Multiprocessor Machine Code[END_REF][START_REF] Owens | A Better x86 Memory Model: x86-TSO[END_REF] focus on the formalisation the x86 model in a proof assistant. A few semantics results are proved on top of the formalisation, as a sanity check. Later on, S. Owens proposed in [START_REF] Owens | Reasoning about the implementation of concurrency abstractions on x86-TSO[END_REF] a generalisation of the DRF guarantee, built on top of the formalisation given in [START_REF] Owens | A Better x86 Memory Model: x86-TSO[END_REF]. Thus, all these previous pieces of work consider one architecture at a time, except [START_REF] Myreen | Verified LISP implementations on ARM, x86, and PowerPC[END_REF], but in this case, only the sequential case is studied, and from the point of view of the instruction set's semantics. By contrast to these previous pieces of work, we provide both a unifying and formalised framework, which nonetheless captures the store atomicity relaxation.

After completing the re-formalisation of the architectures mentioned in section 4, we plan to extend our libraries to the results described in [START_REF] Alglave | Testing for Weak Memory Model Exploration[END_REF][START_REF] Alglave | Stability in Weak Memory Models[END_REF][START_REF] Alglave | A Shared Memory Poetics[END_REF], in a small-scale reflection fashion. We do not expect significant difficulties, since the proofs of these extra results rely on the same techniques as used in the formalisation of [START_REF] Alglave | Fences in Weak Memory Models[END_REF]. Hence the formalisation methods successfully employed in the new library described in the present paper should scale.

Following the approach of M. Myreen et al. [START_REF] Myreen | Verified LISP implementations on ARM, x86, and PowerPC[END_REF][START_REF] Fox | Specification and verification of ARM hardware and software[END_REF][START_REF] Fox | A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture[END_REF], one of the main motivation of the present re-development is actually the design a certifying layer for the tools described in [START_REF] Alglave | Fences in Weak Memory Models[END_REF][START_REF] Alglave | Testing for Weak Memory Model Exploration[END_REF][START_REF] Alglave | Stability in Weak Memory Models[END_REF][START_REF] Alglave | A Shared Memory Poetics[END_REF], e.g. memevents [START_REF] Sarkar | The Semantics of x86-CC Multiprocessor Machine Code[END_REF] and offence [START_REF] Alglave | Stability in Weak Memory Models[END_REF].

The memevents tool [START_REF] Sarkar | The Semantics of x86-CC Multiprocessor Machine Code[END_REF] is a simulator written in OCaml, which, given a small Power or x86 program and a memory model (amongst which the x86 ones from [START_REF] Sarkar | The Semantics of x86-CC Multiprocessor Machine Code[END_REF][START_REF] Owens | A Better x86 Memory Model: x86-TSO[END_REF] and the Power one from [START_REF] Alglave | Fences in Weak Memory Models[END_REF]), outputs all the executions (i .e. the event structures and executions witnesses) of this programm that are allowed by the specified memory model. We would like to validate the specifications implemented in memevents, i .e. make sure that they actually implement the memory model they are supposed to.

We proposed in [START_REF] Alglave | Stability in Weak Memory Models[END_REF] a generalisation of the barrier guarantee (also formalised in Coq), which extends to both lock-based and lock-free synchronisation. We implemented our approach in a tool called offence, which places (upon user's choice) either lock-based or lock-free synchronisation in a program in x86 or Power assembly code. When the chosen primitives are barriers, offence should implement the barrier guarantee, but we would like to validate this. This means that we would like to check that the tool actually places enough barriers in a program to ensure that it will behave as if running on SC.

Yet, while M. Myreen et al. built their tools inside the proof assistant, we would like to use our formalised framework as a correctness checker for the output of the existing external testing tools. The design of such a (large scale) reflexive certificate checker requires to implement and certify inside the Coq proof assistant some efficient algorithms on graphs, e.g. a topological sorting procedure or an acyclicity check. We believe that the preliminary certification of the functional code presented in this paper is a significant step towards the formal certification of a more efficient code, since the remaining effort only lies in the gap between naive and efficient data-structures.

  Variable T : finType. Fixpoint topo_rec (e : rel T) (s : {set T}) (n : nat) := if n is n'.+1 then if [pick x \in s | forallb y, (y \in s) ==> ~~e y x] is Some x then let e' a b := if (a == x) && (b \in (s :\ x)) then true else e a b in topo_rec e' (s :\ x) n' else e else e.

  Lemma topo_rec_anti (e : rel T) (s : {set T}) (s' : {set T}) (ae : {in s' & &, asymmetric e}) (n : nat) : {in s' & &, asymmetric (topo_rec e s n)}.

  Lemma topo_rec_total (e : rel T) (s : {set T}) :acyclic_on s e -> {in s & &, strict_total (topo_rec e s #|s|)}.

  Definition Action := (Dirn * Location * Value). Definition Access d l v : Action := (d, l, v).

  Definition Event_struct := {set Event} * (rel Event). Definition events_of_ES E := let: (evts, _) := E in evts. Definition dp_of_ES E := let: (_, dp) := E in dp. The dp → relation abstracts the instruction semantics 3 . The dp → relation models the dependencies between instructions, e.g. when we compute the address of a load or store from the value of a preceding load. We can compute the program order relation (po E) of an event structure E by the comparing the program indexes of events occurring on the same processor: Definition po (E : Event_struct) : rel Event := [rel e1 e2 | same_proc_same_ES E e1 e2 &&(poi_of_Event e1 <= poi_of_Event e2)].A well-formed event structure E requires dp → to be a subset of the program order. Moreover, since dependencies arise between instructions only when the first one is a load[START_REF][END_REF]26,[START_REF]Alpha Architecture Reference Manual[END_REF], 1], we impose the source of dp → to be always a read.Execution witnesses A given event structure corresponds to several executions of the same program. To model one of these executions, we define execution witnesses. An execution witness X ( ws →, rf →) provides two relations on events, ws → (for write serialisation) and rf → (for read-from map): Definition Execution_witness := (rel Event * rel Event). Definition ws_of_EW (X : Execution_witness) := X.1. Definition rf_of_EW (X : Execution_witness) := X.2.

  Finally we describe a given memory model by implementing what we call its architecture:

	Record Archi : Type := mkArchi{
	ppo : Event_struct -> rel Event;
	grf : Execution_witness -> rel Event;
	ab : Event_struct -> Execution_witness -> rel Event;
	grf_valid : forall X, subrel (grf X) (rf_of_EW X);
	ppo_valid : forall E, subrel (ppo E) (po E);
	ab_evts : forall E X,
	subrel (ab E X) [rel x y \in (events_of_ES E)]}.

An architecture is characterized by its preserved program order ppo → , its global read-from map relation grf → and its barrier semantics

ab

  But this violates the acyclicity hypothesis on r1.Let us now go back to the proof of our the barrier guarantee. Let ghb1 → be the global happens before relation on A 1 . Since (E, X) is valid on A 1 , this relation is acyclic. Let ghb2 → be the global happens before relation on A ǫ 2 . We only need to show that these relations satisfy the hypothesis of acyclicity_crit. Recall from Sec. 3 that for any architecture A we have A.ghb(E, X) . Other possibilities are excluded, for instance by the fact that e 2 cannot be simultaneously a write and a read event. But then we have exactly e 1 grf 2\1 → e 2 , followed by e 2 ppo2 → e 3 , which means that e 1 and e 3 are related by

		ws → ∪	fr → ∪	ppo → ∪	grf → ∪	ab →
	and that for Now suppose that e 1 ghb2 → , ab → is empty by definition. ghb2 → e 2 ghb2 → e 3 but that e 1	ghb1 → e 2 does not hold. In
	that case, under the hypothesis of a valid execution, the only possibility is that e 1 grf2 → e 2 , but not e 1 grf1 → e 2 , and that e 2 ppo2 → e 3 grf 2\1 → ; ppo2 → which is included in ab1 → under the hypothesis A 1 .fb A2 (E, X). Hence e 1 ab1 → e 3 thus e 1 ghb1

http://www.msr-inria.inria.fr/math-components

http://www.comlab.ox.ac.uk/people/jade.alglave/wmm/

We also implement the relation iico between events coming from the same instruction, which we omit here for brevity. For example, a load instruction reads from a location x then writes the contents of x into a register r. In this case, the read event from x and the write event to r are linked by iico. This requires to add register events to the formalism, which is straightforward.

All the results presented here and in[6,

5] hold with a weaker version of uniproc, that allows us to embrace Sun's RMO in our framework. We omit this restriction for clarity and brevity, but more details can be found in[3, p.47-48].

In fact, the execution ex also satisfies the uniproc and thin checks as defined in Sec. 3, but we omit the details for brevity.

Again, we omit the uniproc and thin checks for brevity.

Acknowledgements. We wish to thank Cyril Cohen for his significant help on simplifying the pigeon hole lemma and the proof of the topological sorting.