Armando Castañeda
email: armando.castaneda@im.unam.mx

Aurélie Hurault
email: hurault@enseeiht.fr

Philippe Quéinnec
email: queinnec@enseeiht.fr

Matthieu Roy
email: roy@laas.fr

Tasks in Modular Proofs of Concurrent Algorithms

Keywords: Formal methods, Verification, Concurrent algorithms, Renaming

Proving correctness of distributed or concurrent algorithms is a mind-challenging and complex process. Slight errors in the reasoning are difficult to find, calling for computer-checked proof systems. In order to build computer-checked proofs with usual tools, such as Coq or TLA + , having sequential specifications of all base objects that are used as building blocks in a given algorithm is a requisite to provide a modular proof built by composition. Alas, many concurrent objects do not have a sequential specification.

This article describes a systematic method to transform any task, a specification method that captures concurrent one-shot distributed problems, into a sequential specification involving two calls, set and get. This transformation allows system designers to compose proofs, thus providing a framework for modular computer-checked proofs of algorithms designed using tasks and sequential objects as building blocks. The Moir&Anderson implementation of renaming using splitters is an iconic example of such algorithms designed by composition.

Introduction

Fault-tolerant distributed and concurrent algorithms are extensively used in critical systems that require strict guarantees of correctness [START_REF]Functional safety[END_REF]; consequently, verifying such algorithms is becoming more important nowadays. Yet, proving distributed and concurrent algorithms is a difficult and error-prone task, due to the complex interleavings that may occur in an execution. Therefore, it is crucial to develop frameworks that help assessing the correctness of such systems.

A major breakthrough in the direction of systematic proofs of concurrent algorithms is the notion of atomic or linearizable objects [START_REF] Herlihy | Linearizability: a correctness condition for concurrent objects[END_REF]: a linearizable https://doi.org/10.1007/978-3-030-34992-9_6 object behaves as if it is accessed sequentially, even in presence of concurrent invocations, the canonical example being the atomic register. Atomicity lets us model a concurrent algorithm as a transition system in which each transition corresponds to an atomic step performed by a process on a base object. Human beings naturally reason on sequences of events happening one after the other; concurrency and interleavings seem to be more difficult to deal with.

However, it is well understood now that several natural one-shot base objects used in concurrent algorithms cannot be expressed as sequential objects [START_REF] Castañeda | Unifying concurrent objects and distributed tasks: interval-linearizability[END_REF][START_REF] Hemed | Modular verification of concurrency-aware linearizability[END_REF][START_REF] Neiger | Set-linearizability[END_REF] providing a single operation.

An iconic example is the splitter abstraction [START_REF] Moir | Wait-free algorithms for fast, long-lived renaming[END_REF], which is the basis of the classical Moir&Anderson renaming algorithm [START_REF] Moir | Wait-free algorithms for fast, long-lived renaming[END_REF]. Intuitively, a splitter is a concurrent one-shot problem that splits calling processes as follows: whenever p processes access a splitter, at most one process obtains stop, at most p -1 obtain right and at most p -1 obtain down. Moir&Anderson renaming algorithm uses splitters arranged in a half grid to scatter processes and provide new names to processes. It is worth to mention that, since its introduction almost thirty years ago, the renaming problem [START_REF] Attiya | Renaming in an asynchronous environment[END_REF] has become a paradigm for studying symmetrybreaking in concurrent systems (see, for example, [START_REF] Alistarh | The renaming problem: recent developments and open questions[END_REF][START_REF] Castañeda | The renaming problem in shared memory systems: an introduction[END_REF]).

A second example is the exchanger object provided in Java, which has been used for implementing efficient linearizable elimination stacks [START_REF] Hemed | Modular verification of concurrency-aware linearizability[END_REF][START_REF] Scherer | Scalable synchronous queues[END_REF][START_REF] Shavit | Elimination trees and the construction of pools and stacks[END_REF]. Roughly speaking, an exchanger is a meeting point where pairs of processes can exchange values, with the constraint that an exchange can happen only if the two processes run concurrently.

Splitters and exchangers are instances of one-shot concurrent objects known in the literature as tasks. Tasks have played a fundamental role in understanding the computability power of several models, providing a topological view of concurrent and distributed computing [START_REF] Herlihy | Distributed Computing Through Combinatorial Topology[END_REF]. Intuitively, a task is an object providing a single one-shot operation, formally specified through an input domain, an output domain and an input/output relation describing the valid output configurations when a set of processes run concurrently, starting from a given input configuration. Tasks can be equivalently specified by mappings between topological objects: an input simplicial complex (i.e., a discretization of a continuous topological space) modeling all possible input assignments, an output simplicial complex modeling all possible output assignments, and a carrier map relating inputs and outputs.

Contributions.

Our main contribution is a generic transformation of any task T (with a single operation) into a sequential object S providing two operations, set and get. The behavior of S "mimics" the one of T by splitting each invocation of a process to T into two invocations to S, first set and then get. Intuitively, the set operation records the processes that are participating to the execution of the task. A process actually calls the task and obtains a return value by invoking get. Each of the operations is atomic; however, set and get invocations of a given process may be interleaved with similar invocations from other processes.

We show that these two operations are sufficient for any task, no matter how complicated it may be; since a task is a mapping between simplicial complexes, it can specify very complex concurrent behaviors, sometimes with obscure associated operational semantics.

A main benefit of our transformation is that one can replace an object solving a task T by its associated sequential object S, and reason as if all steps happen sequentially. This allows us to obtain simpler models of concurrent algorithms using solutions to tasks and sequential objects as building blocks, leading to modular correctness proofs. Concretely, we can obtain a simple transition system of Moir&Anderson renaming algorithm, which helps to reason about it. In a companion paper [START_REF] Hurault | Proving a non-blocking algorithm for process renaming with TLA +[END_REF], our model is used to derive a full and modular TLA + proof of the algorithm, the first available TLA + proof of it.

In Sect. 2, we explain the ideas in Moir&Anderson renaming algorithm that motivated our general transformation, which is presented in Sect. 3. Due to lack of space, some basic definitions, proofs and detailed constructions are omitted. They can be found in the extended version [START_REF] Castañeda | Tasks in modular proofs of concurrent algorithms[END_REF].

Verifying Moir&Anderson Renaming

We consider a concurrent system with n asynchronous processes, meaning that each process can experience arbitrarily long delays during an execution. Moreover, processes may crash at any time, i.e., permanently stopping taking steps. Each process is associated with a unique ID ∈ N. The processes can access base objects like simple atomic read/write registers or more complex objects.

The original Moir&Anderson renaming algorithm [START_REF] Moir | Wait-free algorithms for fast, long-lived renaming[END_REF] is designed and explained with splitters. Their seminal work first introduces the splitter algorithm based on atomic read/write registers and discusses its properties. Then, they describe a renaming algorithm that uses a grid of splitters. The actual implementation inlines splitters into the code of the renaming algorithm, and their proof is performed on the resulting program that uses solely read/write registers as base objects.

The Splitter Abstraction. A splitter [START_REF] Moir | Wait-free algorithms for fast, long-lived renaming[END_REF] is a one-shot concurrent task in which each process starts with its unique ID ∈ N and has to return a value satisfying the following properties: (1) Validity. The returned value is right, downor stop.

(2) Splitting. If p ≥ 1 processes participate in an execution of the splitter, then at most p -1 processes obtain the value right, at most p -1 processes obtain the value down, at most one process obtains the value stop. (3) Termination. Every correct process (which doesn't crash) returns a value.

Notice that if a process runs solo, i.e., p = 1, it must obtain stop, since the splitting property holds for any p ≥ 1.

Figure 1 contains the simple and elegant splitter implementation based on atomic read/write registers from [START_REF] Moir | Wait-free algorithms for fast, long-lived renaming[END_REF] (register names have been changed for clarity). After carefully analyzing the code, the reader can convince herself that the algorithm described in Fig. 1 implements the splitter specification. The fact that the implementation is based on atomic registers allows us to obtain a transition system of it in which each transition corresponds to an atomic operation on an object. The benefit of this modelization is that every execution of the implementation is simply described as a sequence of steps, as concurrent and distributed systems are usually modeled (see, for example, [START_REF] Herlihy | The Art of Multiprocessor Programming[END_REF][START_REF] Raynal | Concurrent Programming -Algorithms, Principles, and Foundations[END_REF])). Although the splitter implementation is very short and simple, its TLA + proof is long and rather complex -particularly when considering that it uses a boolean register and a plain register only-(see [START_REF] Hurault | Proving a non-blocking algorithm for process renaming with TLA +[END_REF] for details).

The Renaming Problem. In the M -renaming task [START_REF] Attiya | Renaming in an asynchronous environment[END_REF], each process starts with its unique ID ∈ N, and processes are required to return an output name satisfying the following properties: Let p be the number of processes that participate in a given renaming instance. A renaming implementation is adaptive if the size M of the new name space depends only on p, the number of participating processes. We have then M = f (p) where f (p) is a function on p such that f (1) = 1 and, for 2

≤ p ≤ n, p -1 ≤ f (p -1) ≤ f (p).
Moir&Anderson Splitter-Based Renaming Algorithm. Moir and Anderson propose in [START_REF] Moir | Wait-free algorithms for fast, long-lived renaming[END_REF] a read/write renaming algorithm designed using the splitter abstraction. The algorithm is conceptually simple: for up to n processes, a set of n(n + 1)/2 splitters are placed in a half-grid, each with a unique name, as shown in Fig. 2 for n = 5. Each process starts invoking the splitter at the top-left corner, following the directions obtained at each splitter. When a splitter invocation returns stop, the process returns the name associated with the splitter. We use here an adaptive version of their algorithm that allows p participating processes to rename in at most p(p + 1)/2 names; the original solution in [START_REF] Moir | Wait-free algorithms for fast, long-lived renaming[END_REF] is non-adaptive and the only difference is the labelling of the splitters in the grid.

Splitters as Sequential Objects?

Although Moir&Anderson renaming algorithm is easily described in a modular way, the actual program is not modular as each splitter in the conceptual grid is replaced by an independent copy of the splitter implementation of Fig. 1. Thus, the correctness proof in [START_REF] Moir | Wait-free algorithms for fast, long-lived renaming[END_REF] possible interleavings that can occur, considering all read/write splitter implementations in the grid.

D ← ∅ if |Stop| = 0 then D ← D ∪ {stop} if |Down| < |P articipants| -1 then D ← D ∪ {down} if |Right| < |P articipants| -1 then D ← D ∪ {right} Let dec be any value in D if dec = stop then Stop ← Stop ∪ {id} if dec = down then Down ← Down ∪ {id} if dec = right then Right ← Right ∪ {id} Output: dec endFunction
In the light of the simple splitter based conceptual description, we would like to have a transition system describing the algorithm based on splitters as building blocks, in which each step corresponds to a splitter invocation. Such a description would be very beneficial as it would allow us to obtain a modular correctness proof showing that the algorithm is correct as long as the building blocks are splitters, hence the correctness is independent of any particular splitter implementation.

As it is formally proved in Sect. 3, it is impossible to obtain such a transition system. The obstacle is that a splitter is inherently concurrent and cannot be specified as a sequential object with a single operation. The intuition of the impossibility is the following. By contradiction, suppose that there is a sequential object corresponding to a splitter. Since the object is sequential, in every execution, the object behaves as if it is accessed sequentially (even in presence of concurrent invocation). Then, there is always a process that invokes the splitter object first, which, as noted above, must obtain stop. The rest of the processes can obtain either down or right, without any restriction (the value obtained by the first process precludes that all obtain right or all down). However, such an object is allowing strictly fewer behaviors: in the original splitter definition it is perfectly possible that all processes run concurrently and half of them obtain right and the other half obtain down, while none obtains stop.

The Splitter Task as a Sequential Object. One can circumvent the impossibility described above by splitting the single method provided by a splitter into two (atomic) operations of a sequential object. Figure 3 presents a sequential specification of a splitter with two operations, set and get, using a standard pre/post-condition specification style. Each process invoking the splitter, first invokes set and then get (always in that order). The idea is that the set operation first records in the state of the object the processes that are participating in the splitter, so far, and then the get operation nondeterministically produces an output to a process, considering the rules of the splitter. In Sect. 3, we formally prove that this sequential object indeed models the splitter defined above.

Proving Moir&Anderson Renaming with Splitters as Base Sequential Objects.

Using the sequential specification of a splitter in Fig. 3, we can easily obtain a generic description of the original Moir&Anderson splitter-based algorithm: each renaming object is replaced with an equivalent sequential version of it, and every process accessing a renaming object asynchronously invokes first set and then get, which returns a direction to the process. The resulting algorithm does not rely on any particular splitter implementation, and uses only atomic objects, which allows us to obtain a transition system of it. This is the algorithm that is verified in TLA + in [START_REF] Hurault | Proving a non-blocking algorithm for process renaming with TLA +[END_REF]. The equivalence between the concurrent renaming specification and the sequential set/get specification imply that the proof in [START_REF] Hurault | Proving a non-blocking algorithm for process renaming with TLA +[END_REF] also proves for the original Moir&Anderson splitter-based algorithm.

Dealing with Tasks Without Sequential Specification

In this section, we show that the transformation in Sect. 2 of the splitter task into a sequential object with two operations, get and set, is not a trick but rather a general methodology to deal with tasks without a sequential specification. Our get/set solution proposed here is reminiscent to the request-follow-up transformation in [START_REF] Scherer | Nonblocking concurrent data structures with condition synchronization[END_REF] that allows to transform a partial method of a sequential object (e.g. a queue with a blocking dequeue method when the queue is empty) into two total methods: a total request method registering that a process wants to obtain an output, and a total follow-up method obtaining the output value, or false if the conditions for obtaining a value are not yet satisfied (the process invokes the follow-up method until it gets an output). We stress that the request-follow-up transformation [START_REF] Scherer | Nonblocking concurrent data structures with condition synchronization[END_REF] considers only objects with a sequential specification and is not shown to be general as it is only used for queues and stacks.

Model of Computation in Detail.

We consider a standard concurrent system with n asynchronous processes, p 1 , . . . , p n , which may crash at any time during an execution of the system, i.e., stopping taking steps (for more detail see for example [START_REF] Herlihy | The Art of Multiprocessor Programming[END_REF][START_REF] Raynal | Concurrent Programming -Algorithms, Principles, and Foundations[END_REF]). Processes communicate with each other by invoking operations on shared, concurrent base objects. A base object can provide Read/Write operations (also called register ), more powerful operations, such as Test&Set, Fetch&Add, Swap or Compare&Swap, or solve a concurrent distributed problem, for example, Splitter, Renaming or Set Agreement.

Each process follows a local state machines A 1 , . . . , A n , where A i specifies which operations on base objects p i executes in order to return a response when it invokes a high-level operation (e.g. push or pop operations). Each of these base-objects operation invocations is a step. An execution is a possibly infinite sequence of steps and invocations and responses of high-level operations, with the following properties:

1. Each process first invokes a high-level operation, and only when it has a corresponding response, it can invoke another high-level operation, i.e., executions are well-formed. 2. For any invocation inv( opType, p i , input ) of a process p i , the steps of p i between that invocation and its corresponding response (if there is one), are steps that are specified by A i when p i invokes the high-level operation opType, p i , input .

A high-level operation in an execution is complete if both its invocation and response appear in the execution. An operation is pending if only its invocation appears in the execution. A process is correct in an execution if it takes infinitely many steps.

Sequential Specifications. A central paradigm for specifying distributed problems is that of a shared object X that processes may access concurrently [START_REF] Herlihy | The Art of Multiprocessor Programming[END_REF][START_REF] Raynal | Concurrent Programming -Algorithms, Principles, and Foundations[END_REF], but the object is defined in terms of a sequential specification, i.e., an automaton describing the outputs the object produces when it is accessed sequentially. Alternatively, the specification can be described as (possibly infinite) prefix-closed set, SSpec(X), with all sequential executions allowed by X.

Once we have a sequential specification, there are various ways of defining what it means for an execution to satisfy an object, namely, that it respects the sequential specification. Linearizability [START_REF] Herlihy | Linearizability: a correctness condition for concurrent objects[END_REF] is the standard notion used to identify correct executions of implementations of sequential objects. Intuitively, an execution is linearizable if its operations can be ordered sequentially, without reordering non-overlapping operations, so that their responses satisfy the specification of the implemented object. To formalize this notion we define a partial order on the completed operations of an execution E: op < E op if and only if the response of op precedes the invocation of op in E. Two operations are concurrent if they are incomparable by < E . The execution is sequential if < E is a total order.

An execution E is linearizable with respect to X if there is a sequential execution S of X (i.e., S ∈ SSpec(X)) such that: (1) S contains every completed operation of E and might contain some pending operations. Inputs and outputs of invocations and responses in S agree with inputs and outputs in E, and (2) for every two completed operations op and op in E, if op < E op , then op appears before op in S.

Using the linearizability correctness criteria for sequential objects, we can define the set of valid executions for X, denoted V E(X), as the set containing every execution E that consists of invocations and responses and is linearizable w.r.t. X. V E(X) contains the behavior one might expect from any building-block implementation of X, e.g., any algorithm that implements X.

Tasks. A task is the basic distributed equivalent of a function in sequential computing, defined by a set of inputs to the processes and for each (distributed) input to the processes, a set of legal (distributed) outputs of the processes, e.g., [START_REF] Herlihy | Distributed Computing Through Combinatorial Topology[END_REF].

In an algorithm designed to solve a task, each process starts with a private input value and has to eventually decide irrevocably on an output value. A process p i is initially not aware of the inputs of other processes. Consider an execution where only a subset of k ≤ n processes participate; the others crash without taking any steps. A set of pairs σ = {(id 1 , x 1 ), . . . , (id k , x k )} is used to denote the input values, or output values, in the execution, where x i denotes the value of the process with identity id i , either an input value or an output value. A set σ as above is called a simplex, and if the values are input values, it is an input simplex, if they are output values, it is an output simplex. The elements of σ are called vertices, and any subset of σ is a face of it. An input vertex v = (id i , x i ) represents the initial state of process id i , while an output vertex represents its decision. The dimension of a simplex σ, denoted dim(σ), is |σ| -1, and it is full if it contains n vertices, one for each process. A complex K is a set of simplexes (i.e. a set of sets) closed under containment. The dimension of K is the largest dimension of its simplexes, and K is pure of dimension k if each of its simplexes is a face of a k-dimensional simplex. In distributed computing, the simplexes (and complexes) are often chromatic: vertices of a simplex are labeled with a distinct process identities. The set of processes identities in an input or output simplex σ is denoted ID(σ).

A task T for n processes is a triple (I, O, Δ) where I and O are pure chromatic (n -1)-dimensional complexes, and Δ maps each simplex σ from I to a subcomplex Δ(σ) of O, satisfying: (1) Δ(σ) is pure of dimension dim(σ), (2) for every τ in Δ(σ) of dimension dim(σ), ID(τ ) = ID(σ), and (3) if σ, σ are two simplexes in I with σ ⊂ σ then Δ(σ ) ⊂ Δ(σ). A task is a very compact way of specifying a distributed problem, and indeed typically it is hard to understand what exactly is the problem being specified. Intuitively, Δ specifies, for every simplex σ ∈ I, the valid outputs Δ(σ) for the processes in ID(σ) assuming they run to completion, and the other processes crash initially, and do not take any steps.

As an example consider the splitter task [START_REF] Moir | Wait-free algorithms for fast, long-lived renaming[END_REF]. Figure 4 shows a graphic description of the splitter task for three processes with IDs 1, 2 and 3. The input complex, shown at the left, consists of a triangle and all its faces. The output complex, at the right, contains all possible valid output simplexes (the triangle with all right outputs is not in the complex). The Δ function maps the input vertex with ID 1 to the output vertex (1, stop), the input edge with IDs 1 and 2 to the complex with the bold edges in the output complex, and the input triangle is mapped to the whole output complex. The rest of Δ is defined symmetrically.

Let E be an execution where each process invokes a task I, O, Δ once. Then, σ E is the input simplex defined as follows: (id i , x i ) is in σ E iff in E there is an invocation of task(x i ) by process id i . The output simplex τ E is defined similarly: (id i , y i ) is in τ E iff there is a response y i to a process id i in E. We say that E satisfies (I, O, Δ) if for every prefix E of E, it holds that τ E ∈ Δ(σ E ).

Using the satisfiability notion of tasks we can now consider the set of valid executions, V E(T ), for a given task T = (I, O, Δ): the set containing every execution E that has only invocations and responses and satisfies T . Arguably, the set V E(T ) contains the behavior one might expect from a building-block (e.g. an algorithm) that implements T .

Modeling Tasks as Sequential Objects. Intuitively, tasks and sequential specifications are inherently different paradigms for specifying distributed problems: while a task specifies what a set of processes might output when running concurrently, a sequential specification specifies the behavior of a concurrent object when accessed sequentially (and linearizability tells when a concurrent execution "behaves" like a sequential execution of the object). A natural question is if any task can be modeled as a sequential object with a single operation, namely, the object defines the same set of valid executions. A well-known example for which this is possible is the consensus distributed coordination problem that can be equivalently defined as a task or as a sequential object (see for example [START_REF] Herlihy | The Art of Multiprocessor Programming[END_REF] where it is defined as an object1 and [START_REF] Herlihy | Distributed Computing Through Combinatorial Topology[END_REF] where it is defined as a task).

State: a pair (σ, τ ) of input/output simplexes, initialized to (∅, ∅)

Function set(idi, xi) Pre-condition: idi ∈ ID ∧ idi / ∈ ID(σ) Post-condition: σ ← σ ∪ {(idi, xi)} Output: void endFunction Function get(idi)
Pre-condition: idi ∈ ID ∧ idi / ∈ ID(τ ) Post-condition: Let yi be any output value such that τ ∪ {(idi, yi)} ∈ Δ(σ).

Then, τ ← τ ∪ {(idi, yi)} Output: yi endFunction Fig. 5. A Generic Sequential Specification of a Task T = (I, O, Δ). Lemma 1. Consider the splitter task T spl = (I spl , O spl , Δ spl ). There is no sequential object X spl with a single operation satisfying V E(T spl ) = V E(X spl ).

In a very similar way, one can prove that the following known tasks cannot be specified as sequential objects with a single operation: exchanger [START_REF] Hendler | A scalable lock-free stack algorithm[END_REF][START_REF] Shavit | Elimination trees and the construction of pools and stacks[END_REF], adaptive renaming [START_REF] Attiya | Renaming in an asynchronous environment[END_REF], set agreement [START_REF] Chaudhuri | More choices allow more faults: set consensus problems in totally asynchronous systems[END_REF], immediate snapshot [START_REF] Borowsky | Generalized FLP impossibility result for t-resilient asynchronous computations[END_REF], adoptcommit [START_REF] Borowsky | The BG distributed simulation algorithm[END_REF][START_REF] Gafni | Round-by-round fault detectors: unifying synchrony and asynchrony (extended abstract)[END_REF] and conflict detection [START_REF] Aspnes | Tight bounds for adopt-commit objects[END_REF]. 2To circumvent the impossibility result in Lemma 1, we model any given task T through a sequential object S with two operations, set and get, that each process access in a specific way: it first invokes set with its input to the task T (receiving no output) and later invokes get in order to get an output value from T . Intuitively, decoupling the single operation of T into two (atomic) operations allows us to model concurrent behaviors that a single (atomic) operation cannot specify. In what follows, let SSpec(S) be the set with all sequential executions of S in which each process invokes at most two operations, first set and then get, in that order. Theorem 1. For every task T = (I, O, Δ) there is a sequential object S with two operations, set(id i , x i ) and get(id i ) : y i , such that there is a bijection α between V E(T ) and SSpec(S) satisfying that: (1) each invocation or response of process id i is mapped to an operation of process id i , and (2) each invocation inv (response resp) with input (output) x is mapped to a completed set (get) operation with input (output) x.

An implication of Theorem 1 is that if one is analyzing an algorithm that uses a building-block (subroutine, algorithm, etc.) B that solves a task T , one can safely replace B with the sequential object S related to T described in the theorem (each invocation to the operation of B is replaced with an (atomic) invocation to set and then an (atomic) invocation to get), and then analyze the algorithm considering the atomic operations of S. The advantage of this transformation is that (1) if all operations in an algorithm are atomic, we can think that each process takes a step at a time in an execution, hence obtaining a a transition system with atomic events, (2) at all times we have a concrete state of S in an execution (which is not clear in a task specification) and (3) given a state of S, an output for a get operation can be easily computed using the sequential object S (something that is typically complicated for B as it might be accessed concurrently).

The construction used (for simplicity) in the proof of Theorem 1 (in the full version of the paper) might be too coarse to be helpful for analyzing an algorithm. We would like to have a construction producing an equivalent sequential automaton modeling the task in a simpler way. Consider the simple sequential object in Fig. 5 obtained from any given task T = (I, O, Δ), which is described in a classic pre/post-condition form. Intuitively, the meaning of a state (σ, τ ) is the following: σ contains the processes that have invoked the task so far (this represents the participating set of the current execution) while τ contains the outputs that have been produced so far. The main invariant of the specification is that τ ∈ Δ(σ). It directly follows from the properties of the task: when a process invokes set(id i , x i ), we have that τ ∈ Δ(σ ∪ {(id i , x i )}) because Δ(σ) ⊂ Δ(σ ∪ {(id i , x i )}), and when a process invokes get(id i ), it holds that τ ∪ {(id i , y i )} ∈ Δ(σ) because Δ(σ) is a pure complex of dimension dim(σ) and thus there must exist a simplex in Δ(σ) (properly) containing τ and with an output for id i . One can formally prove that this sequential object and the one in the proof Theorem 1 define the same set of sequential executions.

Finally, one can obtain ad-hoc and equivalent specifications for specific tasks, like the one for splitters in Fig. 3 in Sect. 2.

Related Work

Linearizability Criteria. Neiger observed for the first time that some fundamental tasks, like set agreement [START_REF] Chaudhuri | More choices allow more faults: set consensus problems in totally asynchronous systems[END_REF] and immediate snapshot [START_REF] Borowsky | Generalized FLP impossibility result for t-resilient asynchronous computations[END_REF], cannot be modeled as sequential objects [START_REF] Neiger | Set-linearizability[END_REF] (with a single operation). Motivated by the need of a unified framework for tasks and objects, he proposed set-linearizability [START_REF] Neiger | Set-linearizability[END_REF]. Roughly speaking, a set sequential object is generalization of a sequential object in which transitions between states involve more than one operation (formally, a set of operations), meaning that these operations are allowed to occur concurrently, and their results can be concurrency-dependent. Set linearizability is the consistency condition for set-sequential objects, where one needs to find linearizability points (same as in linearizability) and several operations can be linearized at the same point (different from linearizability).

Later on, it was again observed that for some concurrent objects it is impossible to provide a sequential specification, and concurrency-aware linearizability was defined [START_REF] Hemed | Modular verification of concurrency-aware linearizability[END_REF]. Set linearizability and concurrency-aware linearizability are very closely related, both based on the same principle: sets of operations can occur concurrently. Also, a non-automatic verification technique for reasoning about concurrency-aware objects is presented in [START_REF] Hemed | Modular verification of concurrency-aware linearizability[END_REF].

Recently it was observed in [START_REF] Castañeda | Unifying concurrent objects and distributed tasks: interval-linearizability[END_REF] that some natural tasks specify concurrency dependencies that are beyond the set-linearizability and concurrency-aware formalisms, hence that paper proposed interval linearizability. In an intervalsequential object not only sets of operations can occur concurrently but some of these operations might be pending and then overlap operations in the next transition; thus each operation corresponds to an interval instead of a single point. Interval linearizability is the related consistency condition in which, for each operation, one needs to find an interval in which the operation happens. It is shown in [START_REF] Castañeda | Unifying concurrent objects and distributed tasks: interval-linearizability[END_REF] that interval-linearizability is complete for tasks in the sense that it is possible to specify any task as an interval-sequential object (with a single operation).

Although interval-sequential specifications can model any task, this approach does not seem to be useful when one is searching for machine-checked proofs of concurrent algorithms. The main reason is that by replacing a task with its equivalent interval-sequential object, we obtain a transition system in which one still needs to think in concurrent behaviors, which is usually hard to deal with. In contrast, our proposed get-set transformation allows to "decouple" the inherent concurrency in tasks in a way that in the resulting transition system all events are atomic, namely, they happen one after the other.

Mechanized Verification of Distributed Algorithms. Mechanized (or machineassisted) verification of distributed and concurrent algorithms is usually done with model checking or theorem proving or a combination of both. Enumerative model-checking is the oldest fully automatic method with tools like Spin [START_REF] Holzmann | The SPIN Model Checker -Primer and Reference Manual[END_REF] or TLC, the TLA + model checker [START_REF] Lamport | Specifying Systems[END_REF]. To avoid the well-known problem of state explosion, various optimisations such as symmetry or reduction have been introduced, and recent work is on going on parameterized model checking, for instance with MCMT (Model Checking Modulo Theory) [START_REF] Ghilardi | MCMT: a model checker modulo theories[END_REF], Cubicle [START_REF] Conchon | Cubicle: a parallel SMTbased model checker for parameterized systems[END_REF] or ByMC [START_REF] John | Parameterized model checking of fault-tolerant distributed algorithms by abstraction[END_REF]. Nevertheless, automatic verification of a distributed/concurrent algorithm is still restricted to small finite instances of the algorithm or imposes significant constraints on its description, due to the limited expressiveness of the specification language.

Fully automatic theorem proving is based on a proof decision procedure. For useful logics, it is often semi-decidable at best and heavily depends on heuristics to achieve good performance. Recent work on SMT has made a substantial leap forward checking complex formulae combining first-order reasoning with decision procedures for theory such as arithmetic, equality, arrays. Nonetheless, the overall proof of a distributed algorithm is still largely manual and, when seeking confidence in this proof, an interactive proof assistant is the current approach. Several examples of verification of complex distributed algorithms exist: Chord with Alloy [START_REF] Zave | Using lightweight modeling to understand Chord[END_REF], Pastry with TLA + [START_REF] Lu | Formal verification of the pastry protocol[END_REF][START_REF] Lu | Towards verification of the pastry protocol using TLA +[END_REF], Paxos also with TLA + [START_REF] Lamport | Byzantizing paxos by refinement[END_REF], snapshot algorithms in Event-B [START_REF] Andriamiarina | Revisiting snapshot algorithms by refinement-based techniques[END_REF], just to cite a few.

Several wait-free implementations of tasks have been mechanically proven (e.g. [START_REF] Drȃgoi | Automatic linearizability proofs of concurrent objects with cooperating updates[END_REF][START_REF] O'hearn | Verifying linearizability with hindsight[END_REF][START_REF] Tofan | A compositional proof method for linearizability applied to a wait-free multiset[END_REF]). However, to the best of our knowledge, no non-trivial algorithm built upon concurrent tasks have been mechanically proved. Our intuition for this situation is that proofs cannot be made modular and compositional when using bricks which are inherently concurrent if their internal structure must be visible to take into account this concurrency. Several complex and original algorithms can be found in the literature such as Moir and Anderson renaming algorithm [START_REF] Moir | Wait-free algorithms for fast, long-lived renaming[END_REF] that we have considered in this paper, stacks implemented with elimination trees [START_REF] Shavit | Elimination trees and the construction of pools and stacks[END_REF], lock-free queues with elimination [START_REF] Moir | Using elimination to implement scalable and lock-free FIFO queues[END_REF]. In these papers, the correctness proofs are intricate as they must consider the algorithm as a whole, including the tricky part involving wait-free objects, and they have not been mechanically checked. Our approach which exposes a more simple and sequential specification (instead of a complex concurrent implementation) seeks to alleviate this limitation.

Final Remarks and Future Work

In this paper, we showed a technique to circumvent the known impossibility of specifying a task as a sequential object. Our technique consists in modeling the single operation of the task with two atomic operations, set and get. This transformation leads to a framework for developing transitional models of concurrent algorithms using tasks and sequential objects as building blocks. As a proof of concept, we developed in a companion paper [START_REF] Hurault | Proving a non-blocking algorithm for process renaming with TLA +[END_REF] a full and modular TLA + proof of the Moir&Anderson renaming algorithm [START_REF] Moir | Wait-free algorithms for fast, long-lived renaming[END_REF].

A natural extension of our work is to apply the framework to other concurrent algorithms. Another direction is to extend our techniques to the case of refined tasks and interval-sequential objects, recently defined in [START_REF] Castañeda | Unifying concurrent objects and distributed tasks: interval-linearizability[END_REF]. These two formalisms are generalization of the task and sequential object formalism with strictly more expressiveness; particularly, contrary to the task formalism, refined task are multi-shot, namely, each process may perform several invocations, possibly infinitely many.

A third direction is to study if the duality between the epistemic logic approach and the topological approach shown in [START_REF] Goubault | A simplicial complex model for dynamic epistemic logic to study distributed task computability[END_REF] might be useful in verifying concurrent algorithms. Generally speaking, it is shown in [START_REF] Goubault | A simplicial complex model for dynamic epistemic logic to study distributed task computability[END_REF] that a task can be represented as a Kripke model with an action model, specifying the knowledge obtained by processes when solving the task. It could be interesting to explore how this knowledge could be reflected in our set/get construction and if it could be useful in proving correctness.

Fig. 1 .Fig. 2 .

 12 Fig. 1. Implementation of a Splitter [31]. Fig. 2. Renaming using Splitters.

( 1 )

 1 Validity. The output name of a process belongs to [1, . . . , M]. (2) Uniqueness. No two processes obtain the same output name. (3) Termination. Every correct process returns an output name.

Fig. 3 .

 3 Fig. 3. An ad hoc specification of the Splitter.

Fig. 4 .

 4 Fig. 4. The Splitter Task for Three Processes.

end if.

	initially CLOSED = false
	operation splitter():
	(01) LAST ← my ID;
	(02) if (CLOSED)
	(03)	then return(right)
	(04)	else CLOSED ← true;
	(05)	if (LAST = my ID)
	(06)	then return(stop)
	(07)	else return(down)
	(08)	end if
	(09)

Sometimes, for clarity or efficiency, the object is defined with two operations (in the style of the Theorem 1); however, consensus can be equivalently defined with one operation.

There are non-deterministic sequential specifications of these tasks with unavoidable and pathological executions in which some operations guess the inputs of future operations. See [9, Section 2] for a detailed discussion.

Acknowledgements. Armando Castañeda was supported by PAPIIT project IA102417.


Louis Bigo
email: louis.bigo@ircam.fr

Antoine Spicher
email: antoine.spicher@u-pec.fr

Self-Assembly of Musical Representations in MGS

Keywords: Self-assembly, abstract cellular complexes, MGS, rewriting, pattern matching, Hamiltonian and Eulerian path, pitch space, chord space, tonnetz, all interval series

In this paper, we apply morphogenetic processes, namely self-assembly processes, to compute automatically various abstract spaces that can be used to represent and analyze several well-known musical objects (sequence of chords, interval series, etc.). These constructions have been implemented in MGS, an unconventional programming language belonging to the family of spatial computing languages.

INTRODUCTION

The algebraic nature of many musical formalizations has been very early assessed: from the equal temperament to canon, algebraic objects have been used to study combinatorial properties and classify musical structures. Recently, a fresh look on these structures has emerged focusing on topological or geometrical representations. For example, one can characterize harmonic paths in orbifolds [START_REF] Callender | Generalized voice-leading spaces[END_REF][START_REF] Tymoczko | The geometry of musical chords[END_REF] or build topological spaces embedding musical relationships in their neighborhood relationships [START_REF] Mazzola | The topos of music: geometric logic of concepts, theory, and performance[END_REF].

Following this line of research, we are interested to harness natural morphogenetic processes for building spatial representations of musical objects. To this aim, our work rely on the use of MGS , a domain specific programming language dedicated to the modeling and the simulation of dynamical 1 IJUC˙EM˙05˙Bigo˙V1 1 2 L OUIS BIGO AND ANTOINE SPICHER systems with a dynamical structure [START_REF] Giavitto | Interaction based simulation of dynamical system with a dynamical structure (ds) 2 in mgs[END_REF]. Numerous applications in system and synthetic biology have been developed in MGS and proved that it is a fruitful unconventional tool for (re-)designing algorithms tackling problems embedded in space or having a spatial extension.

In this paper we propose the use of a self-assembly process for studying two paradigmatic problems in theoretical music. This paper is organized as follows. Section 2 provides a brief introduction to the MGS spatial programming language. Section 2.3 exemplifies the use of the MGS concepts by specifying a self-assembly of polymers. This self-assembly process is then hijacked for musical purpose. In Section 3 a combinatorial space is built up enabling the enumeration and the topological classification of All-Interval Series (AIS). Section 4 describes a spatial representation of collections of chords. The paper ends with a conclusion and a discussion about future works.

THE MGS PROGRAMMING LANGUAGE

MGS is a spatial computing programming language developed to enlighten the importance of space in computations [START_REF] Beal | Organizing the aggregate: Languages for spatial computing[END_REF][START_REF]Computing Media and Languages for Space-Oriented Computation[END_REF][START_REF] Scw | the "Spatial Computing Workshops" series and related events. List on the "Spatial Computing Home Page[END_REF]. MGS concepts are based on well established notions in algebraic topology [START_REF] Munkres | Elements of Algebraic Topology[END_REF] and relies on the use of rule based functions, called transformations, to compute declaratively with spatial data structures, called topological collections.

Topological Collections

In MGS , all data structures are unified under the notion of topological collection: an abstract combinatorial complex (ACC) labeled with arbitrary values. The ACC acts as a container and the labels as the elements of the data structure.

More precisely, an ACC K = (C, ≺, [•]) is a set C of abstract elements, called cells [START_REF] Tucker | An abstract approach to manifolds[END_REF], provided with a partial order ≺ called the boundary relation, and with a dimension function [•] : C → N such that for each c and

c ′ in C, c ≺ c ′ ⇒ [c] < [c ′ ]. We write c ∈ K when a cell c is a cell of C.
A cell of dimension p is called a p-cell: 0-cells are points, 1-cells are edges, 2-cells are polygons (e.g., facets in a mesh), etc. For example, a graph is an ACC composed of 0-and 1-cells. Another example is pictured in Figure 1.

The ( p -1)-cells c ′ lower than a p-cell c for the boundary relation ≺ are called the faces of c and we write c Two n-cells are (n, p)-neighbor if they have a common border of dimension p when p ≤ n or if they are in the boundary of a p-cell of higher dimension. A (n, p)-path is a sequence of cells such that two consecutive cells are (n, p)-neighbor. For example, the notion of (0, 1)-path coincides with the usual notion of path in a graph (a sequence of nodes following a route along some edges of the graph.) We call a (n, p)-Hamiltonian path a (n, p)-path visiting each n-cell of an ACC exactly once. Similarly a (n, p)-Eulerian path is a (n, p)-path visiting each p-cell of an ACC exactly once.

′ < c or c > c ′ ; c is called a coface of cells c ′ . We call closure of c in K the sub-complexes c = (C ′ , ≺ ∩ C ′ × C ′ , [•]) where C ′ = {c ′ ∈ C | c ′ ≼ c}.
Finally, a topological collection C is a function that associates a value with a cell in an ACC, see Figure 1. Thus the notation C(c) refers to the value of C on cell c. We write |C| for the set of cells for which C is defined. The collection C can be written as a formal sum c∈|C| v c • c where v c df = C(c). With this notation, the underlying ACC is left implicit but can usually be recovered from the context. By convention, when we write a collection C as a sum

C = v 1 • c 1 + • • • + v p • c p ,
we insist that all c i are distinct. Notice that this addition is associative and commutative. This notation is directly used in MGS to build new topological collections on arbitrary ACC of any dimension.

Transformations

Topological collections are transformed using sets of rules called transformations [START_REF] Spicher | Declarative mesh subdivision using topological rewriting in mgs[END_REF]. A rule is a pair pattern => expression . When a rule is applied on a topological collection, a sub-collection matching with the pattern is replaced by the topological collection computed from expression . There exist several ways to control the application of a set of rules on a collection called rule application strategies. The present work uses solely the maximalparallel strategy: rules are applied as many times as possible without intersection between matched sub-collections.

L OUIS BIGO AND ANTOINE SPICHER

A formal specification of topological rewriting is given in [START_REF] Spicher | Declarative mesh subdivision using topological rewriting in mgs[END_REF]. We only sketch here the part of the patterns language necessary for the comprehension. A pattern variable specifies a cell to be matched in the topological collection together with some optional guard: the expression x / x = 3 matches a cell labeled with the value 3. The guard is the predicate after the symbol / . The variable x can be used in the guard (and elsewhere in the rule) to denote the value of the matched cell or the cell itself, following the context (in case of ambiguity, the variable always denotes the associated value). A pattern is a composition of pattern variables. The composition denoted by a simple juxtaposition (e.g., "x y ") does not constraint the arguments of the composition. Variables can be composed using the (co)face operator: a pattern "x < y " (resp. "x > y ") matches two cells c x and c y such that c x < c y (resp. c x > c y ). Patterns are linear: two distinct pattern variables refer to two distinct cells.

Illustration: Self-Assembly of Cellular Complexes

MGS is a vehicle used to investigate the notions of topological collections and transformations and to study their adequacy to the simulation of various physical, chemical and biological processes [START_REF] Giavitto | Modeling the topological organization of cellular processes[END_REF][START_REF] Giavitto | Topological collections, transformations and their application to the modeling and the simulation of dynamical systems[END_REF][START_REF] Giavitto | Systems Self-Assembly: multidisciplinary snapshots, chapter Simulation of self-assembly processes using abstract reduction systems[END_REF][START_REF] Michel | Rule-based programming for integrative biological modeling -application to the modeling of the λ phage genetic switch[END_REF]. As an example, (local) rewriting rules are particularly adequate to specify self-assembling processes since they mimic closely the incremental and distributed building mechanism of the real phenomenon.

Let illustrate this idea by considering a generic self-assembling process on cellular complexes allowing the building of elaborated spatial structures from a population of basic elements. This process consists in identifying topologically equivalent elements (i.e., cells with the same boundary) in some ACC. This operation is not elementary because the identification must occur at every dimension. A simple way to achieve such computation is to iteratively apply the merge of topological cells that exactly share the same faces until a fixed point is reached. The corresponding topological surgery can be expressed in the MGS syntax as follows: where the primitive new cell p f cf returns a fresh p-cell with faces f and cofaces c f . The rule specifies that two elements x and y whose labels check some arbitrary predicate Pred (given as a parameter) and having the Self-assembly of cellular complexes using transformation Self-Assembly: at first iteration, two matching pair of nodes are merged; then the resulting edges are identified; finally the fixed point is reached.

same faces in their boundaries, merge into a new cell c (that has the union of the cofaces of x and y as cofaces) labeled by a value computed from some arbitrary function Label (given as a parameter). Figure 2 illustrates the process. Figure 3 illustrates the use of transformation Self-Assembly to model a polymerization process. Polymers are long-chained molecules with repeating units called monomers. Monomers react with each other to form polymers in a process called polymerization. Addition polymerization is a particular class of polymerization where monomers combine with polymers in an accretive growth process. Here we consider monomers with two binding sites. A monomer is represented by a rectangular shaped ACC, that is a 2-cell with four edges and four vertices in its boundary. The binding sites correspond to two opposite edges labeled as active. Considering that two active cells can be merged (predicate Pred ) and that they become inactive after merging (function Label ), transformation Self-Assembly builds up polymers as shown in Figure 3. This toy model does not refer to any natural phenomenon but it could be easily extended to manage with real biological data (e.g., modeling the 3-dimensional structure of some DNA strand.) FIGURE 3 Self-assembly of polymers: on the left, the initial population of monomers; on the right, the final polymer seen from two different points of view.

L OUIS BIGO AND ANTOINE SPICHER

SPATIAL INTERPRETATION OF ALL-INTERVAL SERIES

In this section we are interested in the very basics musical notions of pitch and interval. Some 2D ACC is then elaborated by the self-assembly of spatial representation of the twelve interval classes. The combinatorial structure of this space is finally used to enumerate and classify All-Interval Series (AIS).

Backgrounds in Music Theory

In the present work, we are interested in symbolic representation of music. In standard Western music, the usual notation is based on the concept of staff where notes are represented in two dimensions * : vertical height is associated with the pitch of the notes (i.e., how high is the associated sound) and horizontal ordering corresponds to time flow (i.e., when notes have to be played.)

In musical analyses, pitches are often considered up to an octave letting us work with only twelve classes called pitch classes. For example, the pitch class C = {C 0 , C 1 , C 2 , . . . } gathers all the possible Cs. From now on, the term "note" will refer to pitch classes. It is then usual to identify pitch classes to elements of Z 12 (C = 0, C♯ = 1, etc.) such that the difference modulo 12 between two pitch classes exactly corresponds to the number of semitones between the corresponding two notes. All the possible differences constitute the intervals. For example between G = 7 and D = 2, the interval is a perfect fifth corresponding to 2 -7 = -5 ≡ (7 mod 12) semitones. In the following, intervals are refered using the usual notation: P1 = 0 (perfect union), m2 = 1 (minor second or semitone), M2 = 2 (major second), m3 = 3 (minor third), M3 = 4 (major third), P4 = 5 (perfect forth), T T = 6 (tritone), P5 = 7 (perfect fifth), m6 = 8 (minor sixth), M6 = 9 (major sixth), m7 = 10 (minor seventh), M7 = 11 (major seventh).

The identification with intergers of Z 12 provides the set of intervals with an additive group structure, and the natural action of (Z 12 , +) on itself coincides with the transposition operation in music. As an example, the action of the perfect forth transpose A into A + P4 = 9 + 5 ≡ (2 mod 12) = D. The action of each interval on the notes is composed of a variable number of orbits. For an interval i it is well known that the number of orbits is d i = gcd(i, 12). For instance, there are d m3 = gcd(3, 12) = 3 orbits for the minor third:

(C -D♯ -F♯ -A) (C♯ -E -G -A♯) (D -F -G♯ -B)
These cycles can be uniquely identified by an integer between 0 and d i -1 corresponding to the least note of the cycle (e.g., C, C♯ and D for the three cycles above).

Spatial Representation of Interval Classes

In this section, we propose to give a combinatorial construction of the previous formal elements. A usual representation consists of the all-interval circle which is a complete graph with twelve nodes, one for each pitch class. Each edge represents the possible transposition from a note to another under the action of an interval. This structure is represented on left of Figure 4. The allinterval circle has two main drawbacks: (1) it does not distinguish intervals and their inverses (e.g., the edge between C and F represents at the same time a perfect fourth a perfect fifth); (2) each interval is represented many times (one for each note).

We propose to elaborate a more complex structure which exhibits these properties by assembling a population of pieces of space called interval classes. The interval class I i is a topological collection representing interval i. The underlying ACC is composed of a unique 2-cell labeled by i. The faces of this cell include twelve 1-cells also labeled by i. Finally twelve 0cells labeled by the pitch classes constitute the faces of the 1-cells in such a way that two vertices are connected by an edge if their labels are related by the action of i. Top right of Figure 4 illustrates the interval classes associated to perfect fourth and minor third. Note that the boundary of an interval class exibits topologically the orbits of the interval: the number of orbits equals the number of holes +1.

The eleven interval classes -perfect unison is not considered -are then glued together by transformation Self-Assembly which will identify the note (only 0-cells are concerned) with The resulting space is not easily visualizable. Nevertheless, its 1-skeleton (that is the the sub-ACC composed of the n-cells with n ≤ 1) coincides with the all-interval circle.

Application to All-Interval Series

The interval class space has interesting properties which allow the study of musical objects from the point of view of combinatorial topology. It is illustrated in next paragraphs with a study of All-Interval Series (AIS).

All-Interval Series. An AIS is a twelve-tone series including the eleven different intervals. Such series exhibit many notable properties [START_REF] Morris | The structure of all-interval series[END_REF]. One of them is that the first and the last notes are always separated by a tritone interval. One of the most famous use of this particular kind of series is probably on the Lyric Suite of Alban Berg:

& n n n n n n n # n # n # n # n # n
Other composers like Luigi Nono (e.g., Il canto sospeso) or Karlheinz Stockhausen (e.g., Grüppen, Klavierstück IX) used this material in their compositions.

Beyond the simple enumeration of the 46 272 AIS, composers and music analysts have been interested in finding relevant criterions to classify them. André Riotte proposed a classification considering the harmonic content of the AIS. It consists for example in grouping together AIS containing a subsequence corresponding to the notes of particular scales or chords [START_REF] Riotte | Formalismes et modèles musicaux[END_REF]. Elliot Carter investigated a classification enumerating all AIS containing in sequence the complete set of notes included in the All-Triad Hexachord (this 6-chord is the only one containing the twelve possible triads) [START_REF] Schiff | The Music of Elliott Carter[END_REF]. We can also mention an original classification from Franck Jedrzejewski based on knot theory [START_REF] Jedrzejewski | Mathematical Theory of Music[END_REF].

The enumeration and the classification of AIS is a widely known problem in the computing music community. Several computing approaches, more and more optimized, have been used to enumerate all the AIS. One of the first enumeration was done by André Riotte [START_REF] Riotte | Formalismes et modèles musicaux[END_REF] with the help of a FORTRAN program. This enumeration problem has quickly become a classical problem in Constraint Programming [START_REF] Truchet | Musical constraint satisfaction problems solved with adaptive search[END_REF] and is now part of the 50 problems of the CSPLib [START_REF] Gent | CSPLib: a problem library for constraints[END_REF]. Some previous works have been based on the enumeration of the All-Interval Chords, which is a similar problem [START_REF] Otterström | A theory of Modulation[END_REF].

Spatial Structure of AIS.

A naive procedure to collect all the AIS consists in enumerating all the possible permutations of the twelve notes and keeping those exibiting the eleven different intervals. A spatial interpretation of permutation is to look for an Hamiltonian path in the all-interval circle as illustrated in Figure 4 with A. Berg's AIS.

With such a search the 46 272 AIS are lost in the set of 12! candidates. (0, 1)-Hamiltonicity is not a sufficient condition for specifying AIS. An interesting feature of AIS is they are at the same time a permutation of notes and a permutation of intervals. Translated in structural terms, an AIS is a path of the interval class space which is at the same time (0, 1)-Hamiltonian and (0, 2)-Eulerian. It is characterized in a MGS pattern as follows:

n0 < i1 < I1 > i1 > n1 < i2 < I2 > i2 > n2 ... < i11 < I11 > i11 > n11
Two consecutive notes n p ′ and n p with p ′ = ( p -1) have to be (0, 1)neighbors by some interval i p and (0, 2)-neighbors by some interval class I p such that the interval i p belongs to (i.e., is in the boundary of) interval class I p . Linearity of patterns ensures Hamiltonicity. Topological Classification of AIS. Each AIS visits only one 1-cell in the boundary of each 2-cell and this 1-cell belongs to one of the different orbits associated with the interval class. Let then consider the cyclic vector V = (v m2 , . . . , v i , . . . , v M7 ) of an AIS which associates the visited cycle v i with each interval i. For example, the cyclic vector V B of the A. Berg's AIS is

interval class i m2 M2 m3 M3 P5 T T P5 m6 M6 m7 M7 d i 1 2 3 4 1 6 1 4 3 2 1 V B C D♯ C D C D C C C C♯ C
AIS can then be classified by gathering in the same class all the AIS sharing the same cyclic vector. This classification has proved to be of great musical interest [START_REF] Bigo | Building topological spaces for musical objects[END_REF]. For instance, it allows to find AIS including some specific sub-sequence of notes [START_REF] Riotte | Formalismes et modèles musicaux[END_REF][START_REF] Schiff | The Music of Elliott Carter[END_REF]. As an example, the interval content of the harmonic C minor scale C D E♭ F G A♭ B invites us to search for some interesting AIS related to that scale with cyclic vector (C, C♯, D, E, C, F, C, C, C♯, C, C). For example, this class contains the AIS

E D♭ G♭ F B D C A♭ E♭ G A B♭

which exhibits consecutively the seven notes of the scale.

LOUIS BIGO AND ANTOINE SPICHER

Finally, the proposed classification also allows an easy study of AIS up to the standard algebraic operations [START_REF] Morris | The structure of all-interval series[END_REF]: transposition, homothety, retrograde and circular shift. The geometry of the i d i = 3 456 possible classes can be folded into a smaller space of only 72 well identified classes.

SPATIAL REPRESENTATION OF CHORD COLLECTIONS

Chords play an important role in music theory. In this section, we propose to use the self-assembly process of Section 2.3 to build a combinatorial space representing some collections of chords. We first describe this construction, then we show how various spaces investigated in music theory are recovered.

Self-Assembly of Chords

A chord is a collection of pitches played simultaneously. Depending on the context the collection may have different structures: a set of pitches (e.g., an event of a staff), a sequence of pitches (e.g., in a choral), an ordered set of pitch classes (e.g., chord progressions in Jazz), etc. In the following we will consider chords as set of pitch classes and we call p-chord a chord composed of p notes ( p > 0).

Chords as Simplicial Complexes.

Since a p-chord includes 2 p -2 subchords, a p-chord can be represented by a topological collection relying on a (p -1)-simplex. A n-simplex is an ACC of dimension n composed of a unique n-cell c which has exactly n + 1 faces such that for each face c ′ the closure of c ′ is a (n -1)-simplex. The 0-cells are labeled by a single note and other p-cells by the corresponding ( p + 1)-chords. Simplices are often represented geometrically as the convex hull of their vertices as shown in Figure 5 for p-simplices with p ∈ {0, 1, 2, 3}.

3-cell 1-cell {C, E} {E, G} C {C, G} {C, E, G} G E 3-note chord 2-cell 0-cell note 2-note chord 4-note chord FIGURE 5
A chord represented as a simplex. The complex on the right corresponds to first degree I C of the C major tonality and all 2-chords and notes included in it.

Self-Assembly of Chords. Transformation Self-Assembly may act on a given set of chords by identifying n-cells with common labels:

Pred x y = (x = y) Label x y = x
Although these parameters are similar to the previous example, the identification occurs here at any dimension and will result in a simplicial complex (i.e., an ACC made of simplices only).

The following sections give three applications of self-assembly of chords.

Analysis of a Musical Piece

The self-assembly process is generic enough to represent any set of chords.

We propose here to elaborate some space for the study of a piece from its harmonic progression. Figure 6 shows the simplicial complex resulting from the assembly of chords from the eight first measures of Chopin's Prelude 4 Op.28. The complex exhibits neighborhoods between chords but does not give any information about how these chords are ordered in the prelude. A remarkable fact of this ordering is that only one note differs between two consecutive chords. This property holds on the fourteen chords starting from the second one. Being composed of three-note chords, such a progression corresponds to a (2, 1)-Hamiltonian path in the associated simplicial complex: 1-cells neighborhood between two 2-cells represents the two common notes between the chords. This path is partially presented by black arrows for the five first chords, starting from the second one, in Figure 6. The enumeration of all FIGURE 6 Chords of height first measures of Chopin's Prelude 4 Op.28. On the left its simplicial representation. On the right, a path represents the order of chords in a region of the complex. 12 LOUIS BIGO AND ANTOINE SPICHER the possible (2, 1)-Hamiltonian paths in the complex, shows that there exist exactly 120 possible ordering of the chords. But among all these possibilities, the original order used in the Prelude is the one with the smallest distance between chords. Indeed, the interval characterizing the moving note in two consecutive chords is a semitone for all transitions. This example illustrates the topological translation of a well-known compositional strategy called parsimonious voice leading. Chord sequences corresponding to other (2, 1)-Hamiltonian in the complex have been generated with MGS and are available in MIDI format at http://www.lacl.fr/ lbigo/aisb13#analysis.

Tonality Representation

In tonal music, a piece is frequently characterized by the use of successive tonalities. A tonality is defined by a set of notes, each having a particular role. Triadic chords (stacked thirds 3-chords) composed by notes of the tonality are called the degrees of the tonality. As an example, the seven degrees of the C major tonality are:

I C = {C, E, G} I I C = {D, F, A} I I I C = {E, G, B} I V C = {F, A, C} V C = {G, B, D} V I C = {A, C, E} V I I C = {B, D, F}
The self-assembly provides a combinatorial space associated with the tonality. Guérino Mazzola presents in [START_REF] Mazzola | The topos of music: geometric logic of concepts, theory, and performance[END_REF] this topological representation of the diatonic tonality which appears to be a Möbius strip (see Figure 7.) Such a self-assembly process may seem trivial but the elaboration of a space based on chords of higher dimension is difficult by hand. For example tonality may be defined through 4-chords instead of triads (e.g. for C major I C = {C, E, G, B}, I I C = {D, F, A, C}, etc.) After computing the Euler characteristic and the orientability coefficient of the obtained complex for C major characterized by 4-chords, its topology appears to be a toroid (the volume bounded by a torus) which is definitively different from a Möbius strip (e.g., the torus is orientable and the Möbius strip is not.)

C G D A E E B F C I C V C II C V I C IV C V II C III C FIGURE 7
Simplicial representation of C major tonality resulting in a Möbius strip.

Computer Aided Analysis and Composition using

Self-Assembled Spaces In the context of Music Set Theory chords are studied from an algebraic point of view [START_REF] Andreatta | Implementing algebraic methods in openmusic[END_REF]. They are then classified as orbits under the action of some group of transformations. We are here interested in the classification induced by the action of the dihedral group. Using the self-assembly process, we propose to represent each chord class by a simplicial complex. The topology of these classes differ widely from one to another depending on the size of the considered chords and their interval contents. A complete mathematical study of the topologies for 3chords can be found in [START_REF] Catanzaro | Generalized tonnetze[END_REF]. Transformations on musical trajectories. A musical sequence can be represented as a moving object evolving in a space, as the ones illustrated on Figure 8. The static representation of this evolution is a trajectory inside the complex, which consists of sub-complexes representing successive played notes. Figure 9 illustrates two trajectories in a chord class space. Discrete counterparts of some euclidean transformations can be applied on such trajectories. Figure 9 illustrates a discrete π rotation applied on a trajectory representing the first measures of J.-S. Bach's choral BWV 256. The underlying space is the chord class complex built from the assembly of minor and major chords. Moreover a spatial transformation can be applied on the underlying space, rather than on the path. These transformations occur on the labels of the elements only, which means that the topological structure of the underlying space stays unchanged. This property ensures that the aspect of the trajectory is conserved. Some of these spatial transformations have a musical interpretation. For example, a translation leads to a transposition or a modal transposition, depending on the underlying space. A π rotation leads to an musical inversion. Other available transformations lead to alternative musical operations.

Audio results of rotations, translations and transformations of the underlying space, applied to some pieces from various composers (J.-S. Bach, W.A. Mozart, M. Babbit, The Beatles,. . . ) are available in MIDI format at http://www.lacl.fr/ lbigo/aisb13#transformations. Example 5 of the online page corresponds to the transformation illustrated on Figure 9.

HexaChord and PaperTonnetz Software. The previous theoretical considerations have been implemented in two original software based on the notions of generalized Tonnetz and chord class: HexaChord † and PaperTonnetz ‡ .

HexaChord is a computer-aided music analysis environment based on the previous spatial representation of chord classes. Beyond the simple visualization of the different 12 2-dimensional simplicial complexes, HexaChord provides musicologists with three main functionalities on imported midi files:

1. HexaChord computes automatically the best Tonnetze for representing some piece; it is based on the computation of a compliance measure defined at general level on cellular complexes.

2. Giving a particular Tonnetze, HexaChord is able to produce a trajectory from a piece to show interesting geometric properties.

3. Harmonization by spatial criteria is available by adding an extra voice to a set of voices (e.g., a choral) to maximize compliance measurement.

PaperTonnetz [START_REF] Bigo | Papertonnetz: Music composition with interactive paper[END_REF] is a tool that lets musicians explore and compose music with Tonnetz representations by making gestures on interactive paper. It allows composers to discover, improvise and assemble musical sequences in a Tonnetz by creating replayable patterns that represent pitch sequences and/or chords. Figure 10 shows GUI of PaperTonnetz and HexaChord.

CONCLUSION

A notable contribution of this paper is to show that the same generic selfassembly process can be used to build abstract spaces representing various well-known musical objects: the all-interval series, the simplicial representations of chord sets and the associated Tonnetze.

The generic self-assembly process has been implemented in spaces. Then, topological invariants can be computed to investigate and classify them, especially when they have a high dimension.

Works presented here are related to the unconventional computing field in many aspects. First of all, the different computations presented here are specified using topological rewriting, an extension of term rewriting to abstract cellular complexes. Such extension subsumes chemical computing à la Gamma (as commutative-associative rewriting), Lindenmayer systems (as string rewriting) and cellular automata (as a kind of constrained array rewriting). Secondly, the algorithms used are directly inspired by mechanisms investigated in the field of unconventional computing. These mechanisms are used as a very effective heuristic to devise new representations of well known musical objects and processes. For instance, we use self-assembly to build a space associated with a set of chords and we use computations in space to represent and extend musical transformations. Last but not least, from a musical perspective the transformations presented here are highly non conventional. As a matter of fact, the topological framework has been used only very recently to formalize musical notions, while the standard approach relies solely on algebraic structure, e.g., for pitch classes in Set Theory. The topological framework renews our point of view on musical problems and suggests some alternative musical transformations. It also suggests new generative processes to produce music, an area not covered in this paper.

We believe that this preliminary work shows the interest of an expressive and generic framework making possible the systematic building and processing of abstract spaces that appear in musical analysis and theory. Our framework is based on spatial notions developed and studied in algebraic topology, and then amenable to a computer implementation due to their algebraic nature. Initially developed for the modeling and the simulation of dynamical systems, it appears well suited for the musicologist.

Designing original interesting spaces is a first step work. We are currently working on unconventional approaches (e.g., cellular automata, random walk algorithms, etc.) for taking advantage of these spaces for compositional purposes.

FIGURE 1

 1 FIGURE 1On the left, the Hasse diagram of boundary relationship of the ACC given in the middle: it is composed of three 0-cells (c 1 , c 2 , c 3 ), of three 1-cells (e 1 , e 2 , e 3 ) and of a single 2-cells ( f ). The three edges are the faces of f , and therefore f is a common coface of e 1 , e 2 and e 3 . On the right, a topological collection associates data with the cells: positions with vertexes, lengths with edges and area with f .

trans

  Self-Assembly[Pred, Label] = { x y / (Pred x y) and (faces x = faces y) => let c = new cell (dim x) (faces x) (union (cofaces x) (cofaces y)) in (Label x y) * c }

  FIGURE 2Self-assembly of cellular complexes using transformation Self-Assembly: at first iteration, two matching pair of nodes are merged; then the resulting edges are identified; finally the fixed point is reached.

4 8 L

 48 FIGURE 4Spatial representation of AIS. On the left, complete graph topology with A. Berg's AIS in bold. On the top right, spatial representation of the perfect fourth and minor third interval classes (2cells are filled in light gray). On the bottom right, spatial representation using interval classes of the five first elements of A. Berg's AIS.

Figure. 4

 4 on bottom right illustrates the instantiation of this pattern.

Chord

  Classes and Generalized Tonnetze. The dihedral group D 12 allows to gather chords up to transposition and inversion. While transposition T i consists of the action of some interval on the notes of a chord as mentioned above, inversion S considers the inverse of the notes. As an example, (T M3 • S) {C, E, G} = {-C + M3, -E + M3, -G + M3} = {C, E, A}. This action defines 224 equivalent classes of chords.

Figure 8 illustrates 8

 88 FIGURE 8 Assembly of chords equivalent up to transposition and inversion to C Major (C, E, G) (top) and to C7 (C, E, G, B♭) (bottom).

FIGURE 9 A

 9 FIGURE 9A discrete π rotation is applied on a trajectory representing the first measures of J.-S.Bach's choral BWV 256. The underlying space is the chord class complex built from the assembly of minor and major chords.

  MGS ¶ providing a formal and very concise specification. The corresponding MGS transformation has been effectively used to compute and enumerate these † http://vimeo.com/38102171 ‡ http://vimeo.com/40072179

¶ http://mgs.spatial-computing.org LOUIS BIGO AND ANTOINE SPICHER FIGURE 10 Graphical User Interface of PaperTonnetz (top) and HexaChord (bottom).

* We drop here the consideration of duration.

ACKNOWLEDGMENTS

The authors are very grateful to C. Agon, M. Andreatta, G. Assayag, J.-L. Giavitto from the REPMUS team at IRCAM and to O. Michel from the LACL at University of Paris-Est for fruitful discussions. This research is supported in part by the IRCAM and the University Paris Est-Créteil Val de Marne.