Laurent Rodriguez

Jerôme Fellus

Benoît Miramond

Self-organization of reconfigurable processing elements during mobile robots missions

This paper describes a bio-inspired architectural approach to design highly adaptive systems in the context of mobile robotics. The concerned robots evolve in an indoor unknown environment and then exhibit several behaviours such as landscape learning, obstacle avoidance, path planning, sensorimotor control. We aim at designing the intelligent embedded controller of those robots. The controller will be able to selforganize its elements in order to adapt its architecture to the robot behaviour. We focus in this paper on the description of the neural network which was developed to self-organize the system. We present the simulation results of our method.

I. INTRODUCTION

The aim of this work is to design an intelligent embedded controller that will be able to self-organize its elements in order to adapt its architecture to the robot behavior.

Inspired from the feature integration theory [START_REF] Treisman | A feature-integration theory of attention[END_REF], the robot will use three saliency maps. These three maps provide the robot with a sensorimotor cognitive capability in order to react and to adapt its behavior to the environment.

The controller will be able to adapt the size of the different maps according to the states of its actuators and to the saliency of the information from the external environment. As a result of the Kohonen auto-organizing map model [START_REF] Kohonen | Self-Organization and Associative Memory[END_REF], the three saliency maps are constantly competing for the resources of the controller.

In section II we describe the hardware reconfigurable architecture of the controller. After that, in section III we present the self-organizing properties of this system and its behaviour in the context of robotic applications. Then in section IV we present the simulation's results that characterize the behavior of the controller as conclusion.

II. CONTROLLER ARCHITECTURE

The controller is implemented as a single system-on-chip embedded into the robot body. During its life time, the robot exhibits several behaviours that are considered as concurrent processing tasks for the controller. The main goal is then to adapt the number of processing elements of a regular architecture to the current urgency of a task, where urgency is a function of the input-data activity (saliency) as described in section III. The adaptation mechanism is entirely distributed, thus the tasks placement onto the architecture resources is computed on-line by the system itself and does not require any external decision making (local or deported operating system).

The idea is to implement cells as reusable elements which behave as competing neurons in their basic configuration, but can be used by a task as part of its processing. So, each task is implemented as a set of cells. The set of unused cells can be colonized as additional resources to implement bigger tasks. The growing cell sets are thus restricted by the competition between their border cells (see Fig. 1). Since competition is computed from the activity of neighbour neurons (and from input saliency), the geometry of a task in the architecture is not limited to a 2D-rectangle as for standard reconfiguration, but by the number of competing tasks.

As depicted in Fig. 1, the architecture of a cell is thus composed of: direct wiring with its neighbours, a local programmable data-path, a local memory storing program and data, and a configuration port controlled by the local neuron. Four types of information are exchanged in the architecture: the input sensors data on which are computed the different tasks, the results of each processing broadcasted to the neighbours, the program of a replicating cell, and the activities of neurons. The role of these information flows in the selforganizing process is described in the next section.

III. SELF-ORGANIZING MAPS

The concept of self-organization is intrinsically bound to the definition of the Kohonen's maps (p 119 [START_REF] Kohonen | Self-Organization and Associative Memory[END_REF] ). This is particularly interesting for an artificial vision application. The self-organizing map (SOM) is able to order it's elements according to the entry set. This behavior is used to allocate special areas of a computing substrata to the most suitable tasks. As a result of this behavior, we get a data driven allocation process that can be applied to any application fitting this model.

Intrinsically, it is the case of this robotic application where the vision processing is one of the main cognitive action of the robot. For instance, the artificial vision system of our robot stands on a spatiotemporal visual saliency model [START_REF] Verdier | Using High-Level RTOS Models for HW/SW Embedded Architecture Exploration : Case Study on Mobile Robotic Vision[END_REF]. In this model [START_REF] Rahman | GPU implementation of motion estimation for visual saliency[END_REF], the information contained in the input frames are divided in two types: static and dynamic. The first step of the vision process consists in the extraction of the quantity of each of this type of information in order to balance the allocation through the SOM (c.f. Fig. 2). This can be done thanks to a retina-like neural network where a first ON-OFF layer computes the magnitudes of the spatial gradient and a second layer computes the temporal gradient. The robot is also aware of its actuators states. It takes this information into account through another neural network which feeds the third entry of the system shown on Fig. 2.

As the developed SOM converges to an organization that fits the needs of the application, three main areas (in this case study) emerge from the SOM. Each of them are specialized in relation to the different inputs of the system. For instance, the first and the second areas are allocated to compute the static and the dynamic saliency map. The result of the vision maps is to extract the interest points in the image in relation with the shapes and motions in the scene. Finally, a third area is used as a sensorimotor map. This area will merge the informations from the first two areas and from the actuators of the robot in order to learn and to adapt it's behavior relatively to its actions and its environment. The learning process of our SOM can be computed as a cost function minimization problem of the average similarity distance between the input vector and the weight vector. The Manhattan distance in the network topology space between the elected neuron and the learning neuron is used as a criteria of weightiness. A classical "Mexican hat" distribution is then used as a degree of lateral modulation to activate the neurons in a fixed neighborhood and inhibit farther neurons. This choices improve the reactivity of the system and ensure the topological coherency of the network during the adaptation step as illustrated in the following simulations.

IV. RESULTS AND PERSPECTIVES

We developed a simulator of the architecture presented in the previous sections. This simulator can work either with real-time sensors informations from the robot or with recorded data. We presented to the controller architecture the data corresponding to a 3-stages robot indoor mission: A) stationary initialization, B) moving for room exploration and C) stationary landscape learning. As we can see in Fig. 3, the maps compete for the resources (cells) available into the controller according to their inputs. The three stages of the robot mission are clearly visible. From the first to the 200th frame (stage A), the robot remains static and a few objects are moving in front of it. From frames 200 to 490, the robot is moving (stage B). The motion estimation map takes space to the static map. This ensure enough computing power to the motion estimation tasks. Finally (stage C) the robot remains stationary moreover there is no motion in front of it. Therefore the stationary map is gaining space from the dynamic one.

The profiling of the application behavior resulting from simulation is very promising for the next stages of design.

Fig. 1 .

 1 Fig. 1. Architecture of the self-organizing maps.

Fig. 2 .

 2 Fig. 2. Binding from the entries of the neural network to the self-organizing map

Fig. 3 .

 3 Fig. 3. Binding from the entries of the neural network to the self-organizing map


Keywords: trie data structure, collection set abstract data type, performances comparison

Main operations of the Set Collection Abstract Data Type are insertion, research and deletion. A well known option to implement these operations is to use hashtable. Although hashtable does not admit good time complexities in the worst case, the practical time complexities are efficient. Another option is to use the data structure known as the trie. The trie is useful for two main reasons. Firstly, with such a data structure, mentionned operations admit very good theoretical time complexities. Secondly a trie can be seen as a compact representation of a collection of sets since some parts of them are merged together. Aim of this article is to evaluate performances of the trie data structure. The Java language proposes an abstract class corresponding to the Set Collection A.D.T. operations .We propose in this article three different implementations of this abstract class. All of them are variations of the way to manage the sons of nodes. Theoretical complexities are then evaluated. After that, comparison with performances of hashtable are made in different contexts depending of the collection density, the set size and the ground set size. Finally we analyze our results and conclude in which cases the trie structure outperforms others structures.

Introduction

The concept notion as representation of knowledge comes from a real world modelisation. This modelisation supposes a world compounded by object sets having properties (or elements having attributs). The description of a concept summarizes the properties shared by a set of objects. The whole structure gathering and describing a set of concepts of a binary relation (objects/attributes) is known as the Galois lattice of the input relation. This Galois connection has been introduced in the sixties ( [START_REF] Barbut | Ordre et classification[END_REF]). Formal Concept Analysis, as a generalization of the Galois connection, focuses on the mathematization of concept and conceptual hierarchy. The Galois connection corresponding to a binary relation is then seen as a concept lattice of a context where meaning is given to concepts. Mathematical foundations of Formal Concept Analysis can be found in [START_REF] Ganter | Formal concept analysis[END_REF].

In a general point of view, the concept notion could be seen as a couple of sets (intention/extension). By this way the set of concepts is a collection of sets. In the same manner the context itself is a collection of sets. Finally, classical algorithms of lattices construction, of minimal basis or association rules generation manage some set collections. The natural operations to manage such a collection are insertion, research and deletion. By moving together a kind of objects and a set of operations we are able to define an Abstract Data Type (A.D.T.) :

Abstract
a set collection M = {M 1 , M 2 , ..., M m } on a ground set X = {1, 2, ..., n} such that ∀i ∈ [1..m], M i ⊆ X ; Result : a set collection C M = { M ∈I | I ⊆ M}.
Algorithm 1 which solves the previous problem was proposed in [START_REF] Norris | An algorithm for computing the maximal rectangles of a binary relation[END_REF] to compute maximal rectangles of a binary relation. Author of [START_REF] Nourine | A fast algorithm for building lattices[END_REF] have shown how to use it to compute the Hasse diagramm of the lattice of ideals, of the Galois lattice or of the completed Mac Neill lattice of the given relation. The fact is that by using an efficient A.D.T., the algorithm becomes very simple and the implementation trivial.

Algorithm 1: Union closure() Data : a set collection M on a ground set X Result: a set collection C M (C M is closed under union operator.) begin C M = creation() ; for (M ∈ M) do for (C ∈ C M ) do if (not research(C M , C ∪ M ) then insertion(C M , C ∪ M ) ; return C M ; end
One question is then to evaluate the efficiency of the implementation of the operations. We think the efficiency should be supported by three criterions :

-need for memory ; -theoritical time complexity in the worst case ; -practical time complexity ;

The need for memory seems to be noticeable in a F.C.A. context for which the size of set collections could be huge. Moreover the practical studies in [START_REF] Kuznetsov | Comparing performance of algorithms for generating concept lattices[END_REF] has shown once again that a good theoritical complexity does not always lead to practical performances. In particular, this last point was highlighted with the implementation of the Nourine and Raynaud's algorithm ( [START_REF] Nourine | A fast algorithm for building lattices[END_REF]) whose practical performance was disappointing.

The aim of this article is to evaluate the previous three criterions for the data structure known as the trie. The trie is useful for two main reasons. Firstly, with such a data structure, the Set Collection A.D.T. operations admits very good worst case theoritical time complexities. In particular the research operation can be done in a time complexity which does not depend on the collection size. Moreover, these time complexities are easy to compute. Secondly, a trie could be seen as a set collection compact representation since some parts of them are merged together. We will see that this point is measurable. Another well known option to implemente these operations is to use hashtable. Although hashtable does not admit good worst case time complexities, the practical time complexities are efficient. For this reason the practical time complexities evaluation of our three trie implementations will be made by comparison whith hashtable performances. We choose the Java language since this language proposes an abstract class corresponding to the Set Collection A.D.T. operations. Tests will consist only in changing code of the called methods (the program being the same) and measuring the different operations execution time This article is then organized as follows. In the next section we show that the Set Collection A.D.T. is compatible with the abstract class Map of Java language. Then we describe the trie properties and propose three different implementations. In the third section we describe the protocol of comparison test between the different implementations. We then give global results in different tabs depending of the collection density, the sets size and the ground set size. Finally, we conclude our report by listing cases in which the trie structure outperforms others structures.

Abstract Data Type : Map

To simulate the Set Collection A.D.T. we can use a Map A.D.T. similar to the Map interface of Java language. This Map A.D.T. maps keys to values. In case of set collection, the keys are the collection sets. The Map A.D.T. supplies the following operators :

-new() operator : creates a Map object and returns an empty map.

-get(e) operator : returns the value associated to the key e if this key maps a value, otherwise returns Nil. -put(e,value) operator : inserts set e in the map and associates value to it. -remove(e) operator : removes set e in the map. There is a natural equivalence between the previous operators and operators of the Set Collection A.D.T. Main difference is that a value is associated to each set. Even if this value seems useless in general, one has to notice that usually some additional informations are associated to a set : an extention to an intention, a support to a set, a closure to a set... Java language defines an abstract class Map (or Interface) and proposes two main implementations. The first one uses a binary tree (TreeMap) and the other one uses hashtables (HashMap), the key being of any type (the only constraint being existence of a comparison operator). In the following of this article, we propose three new abstract class Map implementations. Each of them take advantage of the fact the key is a set. For this reason these implementations are variations of the tree structure known as the trie. Before describing the different imple-mentations, let us see some formal results about trie (i.d. lexicographic tree).

Lexicographic tree definition

In litterature we often find the structure of trie (i.d. lexicographic tree) to store a set collection M on a ground set X. One constraint of the trie structure is to define an order on elements of X. This structure allows a precise evaluation of insertion, deletion and research operations time complexities. We used these evaluations to proove some complexity results in [START_REF] Medina | Efficient algorithms for clone items detection[END_REF] and [START_REF] Nourine | A fast algorithm for building lattices[END_REF] or [START_REF] Nourine | A fast incremental algorithm for building lattices[END_REF].

Let us give a formal definition of a lexicographic tree corresponding to a set collection.

Definition 1 Let M be a set collection defined over X, with a total order on X denoted by < X . A unique lexicographic tree is associated to M such that :

-Each edge of the tree is labeled with an element of X ; -To each marked node of the tree corresponds a set of M ; -To each set m of M correspond a unique path in the tree (starting from root and ending with a marked node) such that the union of labels in this path corresponds exactly to the set m. -For any path from the root to any node, the order of the successive labels respects the order defined by < X ; -The order of edges leaving a node respects the order defined by < X . Figure 1 gives an example of collection and its associated lexicographic tree.

A boolean can be associated to a node of the tree in order to indicate if the node is marked (i.e. corresponds to a set of the collection and thus to a key) or not. Any field type can be associated to the node for storing the value associated to the key (on marked nodes only).

Lexicographic tree implementation

To test the lexicographic tree performances, we propose three different implementations of the abstract Java class Map. Each of them use the trie structure. The variations concern the choice made to store the children set of each node. Let us now describe the three structures and give the representations corresponding to the collection {abc, ad, bcde} with X = {a, b, c, d, e}.

-ADT MappingList (class ADT L, cf. figure 2) : In that case the children set of a given node is implemented with lists. Each node of the tree contains an element of the ground set X and a list of references to the children nodes of this node. The references are sorted in alphabetical order of elements corresponding to the children nodes refered in list.

When a node has an empty list, there is a mapping value stored in this node corresponding to the mapping object of the set defined by the path for this node. Notice that some nodes could have both a mapping value and a list of children.

Proposition 1 If the children set of a given node is implemented with Lists then : -The put(m,value) operator as an O(|X|) time complexity ; -The get(m) operator as an O(|X|) time complexity ; -The remove(e) operator as an O(|X|) time complexity ;

Access complexity is due to the fact that an element of X appears only once in a set. Cost of a node creation is done in constant time. -ADT MappingTable (class ADT T, cf. figure 3) : In that case the children set of a given node is implemented with an array. Each node of the tree contains an element of X and an array which is indexed by the labels. The entries contain either NIL, if the node has no child corresponding to the label, or reference to the child. For each node, the array size is equal to the X size minus the position of label stored in the node. When a node has an array which all entrie contains NIL, there is a mapping value stored in this node corresponding to the mapping object of the set defined by the path. It is more restricting than the others because of the array fixed size but we will see that this structure gives a better efficiency for the different operators. -ADT MappingMap (class ADT M, cf. figure 4) : In this last case the children set of a given node is implemented using the Java class HashTable. Each node of the tree contains an element of X and an HashMap. HashMap entries contain either NIL, if the node has no child corresponding to the key value of the map, or the reference to a child. The HashMap size is defined by Java and the colisions are managed to have a good efficiency. This class gives no guarantees concerning the map order. In particular, it does not guarantee that the order will remain constant over time. When a HashMap contained on a node is empty, there is a mapping value stored in this node corresponding to the mapping object of the set defined by the path for this node. For this study, we have limited the implementation of the three classes (ADT MappingList/Table/Map) to main operators new(), get(), put( ) and remove( ). A next work will allow to complete these implementations. Use of our classes can be done in the same manner as any other mapping library in Java. Netherveless, the new() operator of the ADT MappingTable admits a different specification. Indeed, each node creation needs to define a tab 2. In figure 2 we compare the need for memory of each implementation for Short collections. In that case, n belongs to [START_REF] Kuznetsov | Comparing performance of algorithms for generating concept lattices[END_REF][START_REF] Nourine | A fast algorithm for building lattices[END_REF] interval and X size is fixed to be equal to 99.

3. Figure 3 and 4 compare the need for memory with X size fixed to be equal to 499 for Short collection and Large collection. All test results concerning Java HashMap and TreeMap are merged since they are similar. One has to notice that all measures are taken when the whole collection is inserted into the structure. A first observation shows that the trie efficiency is proven (with a list or array implementation) in a Full context. A second observation shows that a trie implementation (with list or array) is very competitive in a Short context. But greater is the X size, less the array implementation is efficient. A third observation concerns the case of Large context and of a X size value equal to 499. In that case, for n values smaller than 5 the Java HashTable Map is the more efficient. With n greater than 5 the Java virtual machine has not enough memory to execute the test with our three new implementations.

CPU time executions comparison

We made different tests on CPU time execution for put(), get() and remove() operation to compare the different A.D.T Map implementations. In Tables 1 and2, we compare CPU times execution for HashMap and TreeMap and Tables 3 and4 show CPU times execution for implementations ADT L, ADT M and ADT T. In Tables 1 and3, time measures are carried out on Full collections when the collection size is between 2 12 and 2 20 . For Tables 2 and4, time measures are carried out on Short collections and Large collections. Other tests were made for this study but we only show the most significant one in these Tables. A first look on tables 1 and 2 results shows that, in general, HashMap has better performances than TreeMap for the operation put without taking into account the chosen collections. On Full collections (Table 1), on one hand there is a significant variation of performances on collections with |X| ≤ 15. On the other hand, efficiency variation is not significant for get and remove operations. Then, if we consider the Table 3 and 4 results, we notice that ADT T has appreciably better times than the two others. Nevertheless, the performance of ADT T decreases when the collection sizes or the ground set size grows up. Considering example of Large(5,99) collection in Table 4, we see that put() operator time execution for ADT T is longer than those of ADT L and ADT M. As the same than before, efficiency variation is not significant for get() and remove() operations. Finally, if we consider all results, we observe that CPU time execution for the put() operation depends on the treated collection size. But it doesn't seem to be the same for get and remove operations. This result confirms theoretical evaluation complexity which shows that these operations complexities do not depends of the collection size. But, we do not see significant dependancies of these operations with the ground set size contrary to theoretical evaluations. Times being small and, as a fact, not really significant, we cannot make definitive conclusion on this point.

CPU times (milliseconds)

Conclusion

In this article we have proposed three trie structure implementations. We have evaluated their performances for the Map A.D.T. operations. Theoritical time complexities results make the trie structure the most efficient. Our practical memory measure shows that the ADT MappingTable is very efficient in a dense context. But it becomes unusable when the ground set size grows to 500, the collections sets being large too. Let us note that in that case the ADT MappingList stays competitive. CPU time measures show that in general the ADT MappingTable is the most efficient for the put() operation. Measures for the get() and remove() operations seems to be not significant.

Problem 1

 1 Data Type : Set Collection ; Object : a set collection C = {C 1 , C 2 , ..., C m } on a ground set X ; Operation : -creation() : creates and returns a new empty collection ; -insertion(C, C) : inserts in the collection C the set C ; -research(C, C) : returns "true" if and only if ∃i ∈ [1..m] such that C i = C ; -deletion(C, C) : removes the set C from the collection C ; Let us see in an example how to use this abstract data type. We consider the following generation problem which corresponds to the computation of the closure under union operator of a given collection. Closure under union operator Data input :

Fig. 1 -

 1 Fig.1-Lexicographic tree corresponding to the collection {abc, ad, bcde, cd, cde, e}, with X = {a, b, c, d, e} and < X being the alphabetical order. Circled nodes are the marked nodes corresponding to the collection sets.

Fig. 2 -Proposition 2 Fig. 3 -

 223 Fig.2-Exemple of a lexicographic tree whith the ADT MappingList. The k1, k2, k3 values are the mapping objects corresponding to the set defined by the path in the tree.

Fig. 4 -

 4 Fig.4-Exemple of a lexicographic tree using the ADT MappingMap to store node children. The k1, k2, k3 values are the mapping objects corresponding to the set defined by the path in the tree

Fig 1 :

 1 Fig 1 : Need for memory in case of Full collection with |X| = n.

Fig 2 :

 2 Fig 2 : Need for memory in case of Short collection with |X| = 99.

Figure 3 :

 3 Figure 3 : Need for memory in case of Short collection with |X| = 499.

Figure 4 :

 4 Figure 4 : Need for memory in case of Large collection with |X| = 499.

  Proposition 3 If the children set of a given node is implemented with Maps then :

-The put(m,value) operator as an O(|m| × θ ) time complexity ; -The get(m) operator as an O(|m|) time complexity ; -The remove(e) operator as an O(|m|) time complexity ; θ corresponds to the time needed for the Map allocation (or reallocation) in a new node. One has to notice that the last proposition results do not correspond to worst case time complexity but to practical time complexity.

  Experimental evaluation on Full examples using HashMap and TreeMap Tab. 2 -Experimental evaluation on Short and Large examples using HashMap and

					CPU times (milliseconds)
			ADT L			ADT M			ADT T
	Short(n,p)	put	get remove put	get remove put	get remove
	(3,99)	37	117	92	24	105	124	14	50	25
	(4,99)	147	66	68	231	63	44	97	20	35
	(5,99)	961	185	197	1196	73	35	543	30	35
	(6,99)	10533 164	184	8493	48	40	5823	18	36
	(3,499)	62	290	99	40	32	33	15	25	28
	(4,499)	178	89	105	236	61	68	297	61	71
	(5,499)	1547	132	135	1557	52	39	1183	17	28
	(6,499)	27878 271	237	15873	65	52	14099	40	29
	Large(n,p)	put	get remove put	get remove put	get remove
	(3,99)	91	87	99	82	72		92	80	38
	(4,99)	366	35	39	707	35	17	437	11	20
	(5,99)	5978	72	71	6211	19	24	7467	12	22
	(3,499)	267	79	60	487	57	32	1288	36	24
	(4,499)	2659	223	144	3967	28	24	none none	none
	(5,499)	none none	none	none none	none	none none	none
	TreeMap get remove put get remove 101 90 274 90 28 134 149 put 78 155 639 51 30 265 138 157 792 42 33 484 94 96 981 45 38 1197 67 42 1275 87 71 2366 67 39 2251 91 74 5251 66 41 5692 41 65 12139 66 38 14928 47 52 35770 100 195 34078 65 65 CPU times (milliseconds) ADT L Full(n) 12 13 14 15 16 17 18 19 20 ADT M ADT T put get remove put get remove put get remove 103 71 56 142 27 30 33 9 16 338 45 47 281 10 25 69 9 24 384 35 109 351 11 21 116 9 19 474 34 38 568 11 21 255 11 29 755 28 38 868 11 23 535 11 29 1771 38 47 1480 13 27 1132 12 40 5251 66 41 5692 41 65 3191 28 40 7240 29 49 7407 13 30 6083 12 19 15212 40 41 16310 14 32 12965 11 20 Tab. 3 -Experimental evaluation on Full examples using ADT MappingList, Full(n) 12 13 14 15 16 17 18 19 20 Tab. 1 -TreeMap ADT MappingMap and ADT MappingTable

Tab. 4 -Experimental evaluation on Short and Large examples using ADT MappingList, ADT MappingMap and ADT MappingTable

which size has to be given as parameter. This size depends of the ground set size. For more information, source code and documentation can be found at www.isima.fr/raynaud/.

3 Experimental evaluation -Full collection (Full(n)) : the collection of all sets on ground set X={1,2,...,n} without the empty set. The size of this collection is equal to 2 n . -Short collection (Short(n,p)) : A collection of 10 p sets on ground set X={1,2,..,n} where the size of all sets is short. This size is determined by a probabilistic law. The file is randomly generated. -Large collection (Large(n,p)) : A collection of 10 p sets on ground set X={1,2,..,n} where the size of all sets is long. This size is determined by a probabilistic law. The file is randomly generated. In each example file, sets are generated in alphabetical order and there is no test for set unicity in the collection. The only restriction is the size of the sets. In the following we evaluate time (in millisecond) and memory (in megabytes) performances for the get(), the put() and the remove() operators. The put() operation consists in reading an example file and inserts in a trie each set of the corresponding collection. Note that the CPU time evaluated for this operation takes into account the loading time of the example file. The get and the remove operations are carried out on 10 000 sets randomly chosen without obligation to belong to the tested collection.

"Need for memory" comparison

We made numerous "need for memory" evaluation to compare the different A.D.T. Map implementations. We decide to put in light the most significant of them.

1. In figure 1


Ahmed Bouajjani

Michael Emmi

Gennaro Parlato
email: gennaro@liafa.jussieu.fr

On Sequentializing Concurrent Programs

We propose a general framework for compositional underapproximate concurrent program analyses by reduction to sequential program analyses-so-called sequentializations. We notice the existing sequentializations-based on bounding the number of execution contexts, execution rounds, or delays from a deterministic task-schedule-rely on three key features for scalable concurrent program analyses: (i) reduction to the sequential program model, (ii) compositional reasoning to avoid expensive task-product constructions, and (iii) parameterized exploration bounds. To understand how those sequentializations can be unified and generalized, we define a general framework which preserves their key features, and in which those sequentializations are particular instances. We also identify a most general instance which considers more executions, by composing the rounds of different tasks in any order, restricted only by the unavoidable program and task-creation causality orders. In fact, we show this general instance is fundamentally more powerful by identifying an infinite family of state-reachability problems (to states g1, g2, . . .) which can be answered precisely with a fixed exploration bound, whereas the existing sequentializations require an increasing bound k to reach each g k . Our framework applies to a general class of shared-memory concurrent programs, with dynamic task-creation and arbitrary preemption.

Introduction

Concurrent program analysis is difficult due to the high computational complexity that arises when considering every intricate task interleaving. To avoid such high computational complexity, bounded (underapproximating) exploration is emerging as a general technique. In general, one characterizes a subset of the concurrent program semantics by a bounding parameter k. As k is increased we explore more behaviors, at the expense of more computational resources; in the limit we explore every behavior. A bounded exploration technique is effective when useful information (e.g., the presence of bugs) is obtained by spending a relatively small amount of computational resources (i.e., using low values of k).

By characterizing a subset of the concurrent program semantics by a bounding parameter (e.g., bounded context-switch [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF]), it is often possible to reduce concurrent program exploration to sequential program exploration [START_REF] Qadeer | KISS: Keep it simple and sequential[END_REF][START_REF] Lal | Reducing concurrent analysis under a context bound to sequential analysis[END_REF][START_REF] La Torre | Reducing context-bounded concurrent reachability to sequential reachability[END_REF][START_REF] La Torre | Model-checking parameterized concurrent programs using linear interfaces[END_REF][START_REF] Emmi | Delay-bounded scheduling[END_REF][START_REF] Kidd | One stack to run them all: Reducing concurrent analysis to sequential analysis under priority scheduling[END_REF]-essentially by constructing an equivalent program without concurrency primitives (e.g., task creation, preemption). Such sequentializations are desirable, both practically and theoretically, for several reasons. First, they reduce the exploration problem of any concurrent program to the well-understood model of sequential programs, and are not limited by finite-data programs, per se. Here several practical verification algorithms exist by way of finite-data software model checking [START_REF] Reps | Precise interprocedural dataflow analysis via graph reachability[END_REF][START_REF] Chaudhuri | Subcubic algorithms for recursive state machines[END_REF][START_REF] Ball | The slam project: debugging system software via static analysis[END_REF][START_REF] La Torre | Analyzing recursive programs using a fixed-point calculus[END_REF]), (infinite-state) fixed point computations [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Reps | Weighted pushdown systems and their application to interprocedural dataflow analysis[END_REF][START_REF] Jannet | The Interproc analyzer[END_REF], and (e.g., SMT-based) bounded software verification algorithms [START_REF] Deline | BoogiePL: A typed procedural language for checking object-oriented programs[END_REF][START_REF] Lahiri | Back to the future: revisiting precise program verification using smt solvers[END_REF]. Second, they compute the behavior of each concurrent task compositionallyi.e., without considering the local-state valuations of other tasks. Third, they enable incremental analysis, trading-off computing resources for the amount of explored behaviors, by varying a bounding parameter k ∈ N. (The parameter k determines the (asymptotic) budget of the sequential program exploration. In practice, the reductions add O(k) variables to the resulting sequential program, resulting in an increasingly-expensive (in k) sequential program exploration.) Indeed these sequentialization-based analyses have been applied to discover (in some cases previously-unknown) bugs in device drivers [START_REF] Lal | Reducing concurrent analysis under a context bound to sequential analysis[END_REF][START_REF] La Torre | Reducing context-bounded concurrent reachability to sequential reachability[END_REF][START_REF] La Torre | Model-checking parameterized concurrent programs using linear interfaces[END_REF][START_REF] Lahiri | Static and precise detection of concurrency errors in systems code using SMT solvers[END_REF][START_REF] Emmi | Delay-bounded scheduling[END_REF].

Our principal aim in this work is to develop a theory of parameterized, compositional, concurrent-to-sequential program analysis reductions. Specifically, we make the following contributions:

-To identify the fundamental mechanisms enabling compositional sequentializations, thus formulating a framework in which to define them (Section 3). -To formulate a most general sequentialization in our framework which expresses as many concurrent behaviors as possible (Section 4), while maintaining compositionality, and without extending the class of programs in which tasks are originally written-e.g., by adding unbounded counters. -To classify the existing sequentializations in our framework, and compare them w.r.t. the behaviors explored for their bounding parameters (Section 5).

Besides enlightening the mechanisms which enable sequential reduction, we believe our gained insight can guide further advances, for instance by considering other restrictions to our framework with efficient encodings. Using the three features discussed above ((i) reduction to sequential programs, (ii) compositionality, and (iii) parameterization), the existing sequentializations work by characterizing each concurrent task by an interface of k global-state valuation pairs (where k is the bounding parameter). These k global-state valuation pairs represent a computation of a task which is interrupted k -1 times-the valuations give the initial and final global-states per execution "round." Each task's interface is then computed-in isolation from other tasks-by beginning each round from the guessed global-state valuation, performing a sequence of sequential program steps, then eventually moving to the next round, by updating the current global-state to the next-guessed valuation. Contiguous interfaces (i.e., where the final global-state valuations of one matches the initial valuations of the other) are then glued together to form larger computations. Intuitively, this interface composition builds executions according to a round-robin schedule of k rounds; a complete execution is formed when each i th final global-state of the last task's interface matches the (i + 1) st initial global-state of the first's. When there are a fixed number of statically-created tasks, interfaces are simply composed in task-identifier order. In the more general case, with dynamically created tasks, interfaces are composed in a depth-first preorder over the ordered task-creation tree. (Note by viewing the task-identifier order as the task-creation order, the dynamic case subsumes the static.) Thus, besides features/constraints (i), (ii), and (iii)-which we feel are desirable, and important to maintain for efficiency and scalability of the resulting program analyses-the existing sequentializations are constrained by: (iv) roundrobin executions (in depth-first order on the ordered task-creation tree). Though other schedules can be simulated by increasing the (round) bounding parameter k when the number of tasks is bounded, for a fixed value of k, only k-round round-robin schedules are explored.

The most general instance of the framework we propose in Section 4 subsumes and extends the existing round-robin based (i.e., context-and delay-bounded) sequentializations. As in these previous approaches, we restrict ourselves to explorations that are (i) sequential, (ii) compositional, and (iii) parameterized, in order to compute task interfaces over k global-state valuation pairs. However, for the same analysis budget1 (i.e., the bounding parameter k), the general instance expresses many more concurrent behaviors, essentially by relaxing the round-robin execution order, and decoupling each task from any global notion of "rounds." We consider that each task's interface is constructed by composing the rounds of tasks it has created in any order that respects program order, and task-creation causality order-i.e., a task is not allowed to execute before a subsequent preemption of the task that created it. Thus the simulated concurrent execution need not follow a round-robin schedule, despite the prescribed task traversal order; the possible inter-task interleavings are restricted only by the constraint that at most k sub-task round summaries can be kept at any momentindeed this constraint is necessary to encode the resulting sequentialization with a bounded number of additional (finite-domain) program variables.

In fact, the most general instance of our framework is fundamentally more expressive than the existing sequentializations, since there are infinite sequences of states (e.g., g 1 , g 2 , . . .) which can be reached with a fixed exploration bound, whereas the existing sequentializations require an increasing bound k to reach each g k . This gain in expressiveness may or may not be accompanied by an analysis overhead. For enumerative program analysis techniques (e.g., model checking, systematic testing), one may argue that considering more interleavings will have a negative impact on scalability. This argument is not so clear, however, for symbolic techniques (e.g., SMT-based verification, infinite-state fixed-point computations), which may be able to reduce reasoning over very many interleavings to very few, in practice [START_REF] Lal | Reducing concurrent analysis under a context bound to sequential analysis[END_REF]. Although many device driver bugs have been discovered within few interleavings [START_REF] Musuvathi | Iterative context bounding for systematic testing of multithreaded programs[END_REF], reducing the number of interleavings could indeed cause missed bugs in other settings. Furthermore, our hope is that enlightening the mechanisms behind sequentialization will lead to the discovery of other succinctly-encodable instances of compositional sequentialization.

Concurrent Programs

We consider a simple but general concurrent programming model in the style of single-threaded event-driven programs. (The style is typically used as a lightweight technique for adding reactivity to single-threaded applications by breaking up long-running computations into a collection of tasks.2 ) In this model, control begins with an initial task, which is essentially a sequential program that can read from and write to global (i.e., shared) storage, and post additional tasks (each post statement specifies a procedure name and argument) to an initially empty task buffer of pending tasks. When control returns to the dispatcher, either when a task yields control-in which case it is put back into the task buffer-or completes its execution, the dispatcher picks some task from the task buffer, and transfers control to it; when there are no pending tasks to pick, the program terminates. This programming model is powerful enough to model concurrent programs with arbitrary preemption and synchronization, e.g., by inserting a yield statement before every shared variable access.

Let Procs be a set of procedure names, Vals a set of values containing true and false, and T the sole type of values. The grammar of Fig. 1 describes our language of asynchronous programs, where p ranges over procedure names. We intentionally leave the syntax of expressions e unspecified, though we do insist the set of expressions Exprs contains Vals and the (nullary) choice operator . The set of program statements s is denoted Stmts. A sequential program is an asynchronous program which contains neither post nor yield statements.

A (procedure-stack) frame , s is a valuation ∈ Vals to the procedure-local variable l, along with a statement s to be executed. (Here s describes the entire body of a procedure p that remains to be executed, and is initially set to p's top-level statement s p .) A task w is a sequence of frames representing a procedure stack, and the set (Vals × Stmts) * of tasks is denoted Tasks. An (asynchronous) = e[g/g, /l] e -since g and l are the only variables, the expression e[g/g, /l] has no free variables. To select the next-scheduled statement in a configuration, we define a statement context S as a term derived from the grammar S ::= | S; s, and write S[s] for the statement obtained by substituting a statement s for the unique occurrence of in S.

The transition relation → a P of an asynchronous program P is defined in Fig. 2 as a set of operational steps on configurations. The transition relation → s P for the sequential program statements (see Appendix C) is standard. The Post rule gives a newly-created task to the task buffer, while the Yield rule gives the currently-executing task to the task buffer. The Dispatch rule chooses some task from the buffer to execute, and the Complete rule disposes a completed task.

A configuration g, , s , ∅ is called initial, and is sequential when s does not contain post (nor yield) statements. An (asynchronous) execution of a program P (from c 0 to c j ) is a configuration sequence h = c 0 c 1 . . . c j where c 0 is initial, and c i → a P c i+1 for 0 ≤ i < j. We say a configuration c = g, w, m (alternatively, the global value g) is reachable in P (from c 0 ) when there exists an execution of P from c 0 to c. The asynchronous semantics of P , written {|P |} a , maps initial configurations to reachable global values, i.e., {|P |} a (c 0 ) = g if and only if g is reachable in P from c 0 . When P is a sequential program, the sequential semantics of P , written {|P |} s , maps initial sequential configurations to reachable global values.

Compositional Semantics

Here we define a compositional semantics for asynchronous programs on which to base our reduction to sequential programs. To do so, we characterize each posted task by an interface exposing only global-state valuations to other tasks. Each interface summarizes not only the computation of a single task, but also the computations of all descendants of tasks it has posted. In particular, an interface is a sequence g 1 , g 1 . . . g k , g k of global-state valuation pairs summarizing a computation which is interrupted k -1 times; the computation begins with global state g 1 , is interrupted by an external task at global state g 1 , is resumed at g 2 , etc. We call the computation summarized by each pair g i , g i the i th round. A larger computation is then formed from a collection of task interfaces, by gluing together contiguous rounds (e.g., summarized by g 1 , g 2 and g 2 , g 3 ), while maintaining the order between rounds from the same interface.

We construct interfaces inside a data-structure called a summary bag. Besides the sequence B ex of rounds which will be exported as the current task's interface (see Fig. 3a), the bag maintains a collection B im of interfaces imported from posted tasks (see Fig. 3c). At any yield-point, the current task can begin a new round, by guessing3 the global-state valuation that will begin the next round (see Fig. 3b), or, if the current global-state valuation matches the start of the first unconsumed round from some imported interface (as does a, b in Fig. 3d), the current task can consume that round and update the current global state; this amounts to interleaving the round of a posted task at the current control point.

With this view of recursive interface construction-interfaces are constructed from interfaces of sub-tasks-the reduction to sequential programs is nearly straightforward. To compute the imported summary of a posted task, we translate the post statement into a procedure call which returns the computed interface for the posted task. At yield points, we will repeatedly, nondeterministically choose to begin a new round, consume a round from an imported interface, or step past the yield statement. For the moment the only obstacle is how to store the unbounded summary bag; we address this issue in Section 4.

To define the compositional semantics we formalize the summary-bag operations. A summary bag B = B ex , B im pairs the round sequence B ex to be exported from the current task, along with a collection B im of round sequences imported from sub-tasks. The empty bag B ∅ = ε, ∅ is an empty sequence paired with an empty collection. The operations to add the current round (⊕), import a sub-task interface ( ), and consume a sub-task round ( ) are defined as

B ex , B im ⊕ g, g def = B ex • g, g , B im , add round B ex , B im B ex def = B ex , B im ∪ B ex , import interface B ex , B im g, g def = B ex , B im consume round,
where B im is obtained by removing g, g from the head of a sequence in B im , and B ex , B im g, g is undefined if g, g is not at the head of B im . We define the compositional transition relation of asynchronous programs by augmenting the sequential transitions → s P with a new set of transitions for the asynchronous control statements, over a slightly different notion of configuration. In order to build interfaces, each configuration carries the global-state valuation at the beginning of the current round (denoted g 0 below), as well as the current the task-summarization relation . We say a configuration c = g 0 , g, w, B (alternatively, the global value g) is reachable in P (from c 0 ) when there exists an execution from c 0 to c, without using the NextRound rule. 4 The compositional semantics of P , written {|P |} c , maps initial configurations to reachable global values, i.e., {|P |} c (c 0 ) = g if and only if g is reachable in P from c 0 .

Although their definitions are wildly different, the compositional and asynchronous semantics are equivalent. To see that every asynchronous execution h has a corresponding compositional execution, consider, inductively, how to build the interface summarizing the projection of h a given task's sub-task segments. Consider the task A of Fig. 5 which posts B and C. To simulate the asynchronous (sub-) execution of Fig. 5a, A builds an interface with two uninterruptible rounds (see Fig. 5c): the first sequencing segments 1 and 2, and the second sequencing 3, 4, 5, and 6. To build this interface, A must import two-round interfaces from B and C each; note that each round of B and C may recursively contain many interleaved segments of sub-tasks.

Theorem 1. The compositional semantics and asynchronous semantics are identical, i.e., for all programs P we have {|P |} c = {|P |} a . 5The proof to this theorem appears in Appendix B.

Bounded Semantics

As earlier sequentializations have done by constraining the number of rounds [START_REF] Lal | Reducing concurrent analysis under a context bound to sequential analysis[END_REF][START_REF] La Torre | Reducing context-bounded concurrent reachability to sequential reachability[END_REF], by constraining the size of the summary bag, we can encode the bag contents with a fixed number of additional variables in the resulting sequential program. Since we are interested in exploring as many behaviors as possible with a limitedsize bag, an obvious point of attention is bag compression. Thus we define an additional operation to free a space in the bag by merging two contiguous (w.r.t. the global valuation) summaries, essentially removing the possibility for future reordering between the selected segments. In doing so, we must maintain causal order by ensuring the bag remains acyclic, and what was before a collection B im of summary sequences imported from sub-tasks now becomes a directed acyclic graph (DAG) of summaries. To maintain program order in the presence of merging, summaries are now consumed only from the roots of B im .

The size

|B| def = |B ex | + |B im | of B
is the sum of the length of the sequence B ex and the number of nodes of the DAG B im . The bag simplification operation B ex , B im B ex , B im obtains B im from B im by merging two nodes n and n , labelled, resp., by g 1 , g 2 and g 2 , g 3 , such that either (a) there is no directed path from n to n in B im , or (b) there is an edge from n to n in B im (see Fig. 6); in either case the merged node is labelled g 1 , g 3 . Note that when B B we have |B | = |B| -1. Though we could simulate this merge operation in the (unbounded) compositional semantics, by eventually consuming consecutively n and n into the exported summary list, the merge operation allows to eagerly express the interleaving-though disallows any subsequent interleaving between n and n . Merging summaries eagerly fixes a sequence of inter-task execution segments, trading the freedom for external interleaving (which may have uncovered additional, potentially buggy, behaviors) for an extra space in the bag.

We define the k-bounded compositional semantics of P, written {|P |} k c , by restricting the compositional semantics {|P |} c to executions containing only configurations g 0 , g, w, B such that |B| ≤ k, and adding the additional transition Compress B B g 0 , g, w, B → c P g 0 , g, w, B

.

As we increase k, the set of k-bounded semantics grows monotonically, and in the limit, the k-bounded semantics is the compositional semantics. For two functions f, g : A → ℘(B), we write f ⊆ g when for all a ∈ A, f (a) ⊆ g(a). Theorem 2. The sequence of bounded compositional semantics forms a monotonically increasing chain whose limit is identical to the compositional semantics, i.e., {|P |} 0

c ⊆ {|P |} 1 c ⊆ . . . ⊆ k∈N {|P |} k c = {|P |} c .
Remark For simplicity, we present a compositional semantics in which information (i.e., the summary bags) only flows up from each sub-task to the task that posted it. However, an even more compact semantics-in the sense that more behaviors are expressed with the same bag-size bound-is possible when each task not only returns summaries, but also receives summaries as a parameter. For example, to interleave 2k summaries of two sub-tasks, one can pass the k summaries of the first sub-task to the second, and merge them with the second's summaries, as they are created, keeping only k at a time. Otherwise, one must interleave the two tasks' summaries outside, which means keeping 2k summaries for the enclosing task to interleave. Since the extension is purely technical, and not so insightful, we omit its description here. However, the results stated in the remainder of this paper are presented in terms of the bag-size bound w.r.t. this extension.

Note on Complexity

For the case where variables have finite-data domains, determining whether a global valuation is reachable is NP-complete6 (in k) for the bounded-task k-context bounded and unbounded-task k-delay bounded sequentializations [START_REF] Lal | Reducing concurrent analysis under a context bound to sequential analysis[END_REF][START_REF] Emmi | Delay-bounded scheduling[END_REF], and PSPACE-complete (in k) for the unbounded-task k-context bounded sequentialization [START_REF] La Torre | Model-checking parameterized concurrent programs using linear interfaces[END_REF]. Since these cases are reducible to our semantics (see Section 5), it follows that global-state reachability is PSPACE-hard (in k) in the most general instance of our framework. Since the number of bag configurations is (singly) exponential in k, membership in EXPTIME is not hard to obtain. The practical difference between the NP/PSPACE-complete complexities of other sequentialization-based analyses is unclear; as sub-exponential time algorithms are not known for NP problems, exponential time is spent in the worst case, either way. Note however, that these complexity considerations are of limited significance, since we target an arbitrary class of sequential programs-not only programs with finite-data.

Global-Round Explorations

To understand the relationship between our bounded compositional exploration and the existing sequentializable analyses, we proceed in two steps. First we describe a restriction of our bounded semantics in which every task agrees on a global notion of execution "rounds," i.e., where each task executes (at most) one uninterrupted segment per global round. Second we show that this restriction captures and unifies the existing sequentializable analyses based on bounded context-switch and bounded delay.

A k global-round execution of a program P is an asynchronous execution of P where (i) each task executes in (up to) k uninterrupted segments called "rounds"-with the restriction that sub-tasks can only execute in, or after, the round in which it is created-and (ii) the i th round of every task is executed before the (i + 1) st round of any task, in the depth-first order over the task-creation tree; see Fig. 7a. Thus we can view each task as executing across a grid of k rounds, being interrupted k -1 times by the other tasks. With this view, each task can be characterized by an interface consisting of 2k global state valuations: the k global-state valuations seen by the task at the beginning of each round, and the k global-state valuations seen at the end (as in Fig. 7a). A task's interfaces are computed by guessing the initial global-state valuation of each round, following some number of sequential transitions, then nondeterministically advancing to the next round, keeping the computed local state, but updating the global-state to the next-guessed valuation. Given the interfaces for each task, sequentialization of the k global-round schedules is possible, by a reduction that executes each task once, according to the linear task-order, over a k-length vector of global-state valuations. The k global-round semantics of P , written {|P |} k gr is the set of global valuations reachable in a k global-round execution of P .

Though we have defined the global-round semantics w.r.t. the asynchronous semantics, in fact we can restrict the k-bounded compositional semantics to compute only k global-round interfaces. During construction of the j th roundsummary of the current task t, the export-list contains j -1 summaries (of rounds 1 . . . j -1) for t and its current sub-tasks, i.e., all descendants of t's thus-far posted tasks. At the same time, the bag maintains a (k -j + 1)-length list of summaries accumulating the rounds j . . . k of t's current sub-tasks. Just before t begins round j + 1, the accumulated summary of round j for t's current sub-tasks is consumed, so that the exported summary of round j captures the effect of one round of t, followed by one round of t's current sub-tasks. When t posts another task t i (in round j), the k -j + 1 summaries exported by t i -note t i and its descendants can only execute after round j of t-are combined with the k -j + 1 accumulated summaries of t's current sub-tasks. 7 Thus when t completes round k, each round i summarizes round i of t followed by round i of each sub-task of t, in depth-first order, over the ordered task-creation tree of t. In fact, our compositional semantics captures many more behaviors than k global-round analyses. For example, many behaviors cannot be expressed in k (global) rounds, though can be expressed by decoupling the rounds of different tasks. Intuitively, the additional power of our compositional semantics is in the ability to reuse the given bounded resources locally, ensuring only that the number of visible resources at any point is bounded. Appendix D illustrates an example demonstrating this added analysis power.

Theorem 4. There exists a program P , k 0 ∈ N, and a sequence g 1 , g 2 , . . . ∈ {|P |} k0 c of global-state valuations such that for all k ∈ N, g k / ∈ {|P |} k gr .

Context-bounding

In its initial formulation, the so-called "context-bounded" (CB) analyses explored the asynchronous executions of a program with a fixed number of statically allocated tasks, with at most two context-switches between tasks [START_REF] Qadeer | KISS: Keep it simple and sequential[END_REF]. Shortly thereafter, Qadeer and Rehof [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF] extended CB to explore an arbitrary bound k of context-switches. Later, Lal and Reps [START_REF] Lal | Reducing concurrent analysis under a context bound to sequential analysis[END_REF] proposed a linear "round-robin" task-exploration order, and instead of bounding the number of context-switches directly, bounded the number of rounds in an explored round-robin schedule between n tasks. (It is easy to see that every k-context bounded execution with an unrestricted scheduler is also a k-round execution with a round-robin scheduler.) With this scheduling restriction, it becomes possible to summarize each task i's execution by an interface of k global-state valuation pairs, describing a computation that is interrupted by tasks (i + 1), (i + 2), . . . , n, 1, 2, . . . , (i -1), k -1 times. In fact, this schedule is just a special case of the k global-round exploration, restricted to programs with a fixed number of statically-created tasks. La Torre et al. [START_REF] La Torre | Model-checking parameterized concurrent programs using linear interfaces[END_REF]'s subsequent extension of this k-round round-robin exploration to programs with a parameterized amount of statically-created tasks is also a special case of k global-round exploration, restricted to programs with an arbitrary number of statically-created tasks.

To formalize this connection, let a static-task program be an asynchronous program P which does not contain post statements, and an initial configuration g, , s , ∅ is (resp., parameterized) static-task initial when s is of the form post p 1 (); ...; post p n () (resp., while do post p ()).

A k-round (resp., parameterized) CB execution of a static-task program P is an asynchronous execution of P from a (resp., parameterized) static-task initial configuration c 0 , where the initially posted tasks are dispatched in a round robin fashion over k rounds. The k-round (resp., parameterized) CB semantics of P , written {|P |} k cb (resp., {|P |} k cb * ) is defined, as before, as the set of global valuations reachable from c 0 in a k-round (resp., parameterized) CB execution of P .

Theorem 5. The k-round (parameterized) CB semantics is equal to the k globalround semantics, i.e., for all static-task programs P we have {|P |} k cb ( * ) = {|P |} k gr .

Delay-bounding

Emmi et al. [START_REF] Emmi | Delay-bounded scheduling[END_REF]'s recently introduced delay-bounded (DB) exploration8 expands on the capabilities of Lal and Reps [START_REF] Lal | Reducing concurrent analysis under a context bound to sequential analysis[END_REF]'s k-round CB exploration with its ability to analyze programs with dynamic task-creation (i.e., with arbitrary use of the post statement). Like CB, the DB exploration considers round-based executions with a linear task-exploration order, though with dynamic task-creation the order must be defined over the task-creation tree; DB traverses the tree depth-first.

In fact, Emmi et al. [START_REF] Emmi | Delay-bounded scheduling[END_REF]'s delay-bounded semantics is a variation of the k globalround semantics which, for the same bound k, expresses many fewer asynchronous executions. In essence, instead of allowing each task k-1 interruptions, the budget of interruptions is bounded globally, over the entire asynchronous execution; see Fig. 7b. It follows immediately that each task executes across at most k rounds, in the same sense as in the k global-round semantics. Since the mechanism behind delay-bounding is not crucial to our presentation here, we refer the reader to Emmi et al. [START_REF] Emmi | Delay-bounded scheduling[END_REF]'s original work for the precise definition of k-delay executions. The k-delay semantics of P , written {|P |} k db is the set of global valuations reachable in a k-delay execution of P . Theorem 6. The k-delay semantics is subsumed by the k global-round semantics, i.e., for all programs P we have {|P |} k db ⊆ {|P |} k gr .

However, like the separation between k-global round semantics and k bounded semantics, there are families of behaviors that can be expressed with a fixed number of global rounds, though cannot be expressed with a fixed number of delays: for instance, behaviors which requires an unbounded number of tasks be interrupted (once) cannot be expressed with any finite number of delays.

Theorem 7. There exists a program P , k 0 ∈ N, and a sequence g 1 , g 2 , . . . ∈ {|P |} k0 gr of global-state valuations such that for all k ∈ N, g k / ∈ {|P |} k db .

Context-bounding vs. Delay-bounding

It follows from Theorems 5 and 6 that context-bounding simulates delay-bounding on static-task programs. In fact, we can also show that delay-bounding simulates context-bounding, for programs with a fixed number of tasks, by combining Theorem 5 with the following theorem.

Theorem 8. For a fixed number n of tasks, the k global-round semantics is subsumed by the nk-delay semantics, i.e., for all static-task programs P with n-tasks we have {|P |} k gr ⊆ {|P |} nk db .

However, by Theorems 5 and 7, delay-bounding cannot simulate k-round parameterized context-bounded executions, since no fixed number of delays can express the unbounded number of potential context-switches.

Related Work

The technique of reducing a concurrent program behaviors to sequential program behaviors has garnered much attention in recent years. Based on the notion of context-bounding [START_REF] Qadeer | KISS: Keep it simple and sequential[END_REF][START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF][START_REF] Musuvathi | Iterative context bounding for systematic testing of multithreaded programs[END_REF], Lal and Reps [START_REF] Lal | Reducing concurrent analysis under a context bound to sequential analysis[END_REF] showed how to encode the bounded-round round-robin schedules of a concurrent program with statically-allocated tasks as a sequential program. La Torre et al. [START_REF] La Torre | Reducing context-bounded concurrent reachability to sequential reachability[END_REF] gave a more efficient encoding-in the sense that unreachable global-state valuations are never explored-and later extended the approach to programs with an unbounded number of statically-allocated tasks [START_REF] La Torre | Model-checking parameterized concurrent programs using linear interfaces[END_REF]. Emmi et al. [START_REF] Emmi | Delay-bounded scheduling[END_REF] have recently extended the basic insight of round-based scheduling to sequentialize programs with an unbounded number of dynamically-created tasks. Empirical evidence suggests such techniques are indeed useful for bug-finding [START_REF] Musuvathi | Iterative context bounding for systematic testing of multithreaded programs[END_REF][START_REF] Lahiri | Static and precise detection of concurrency errors in systems code using SMT solvers[END_REF][START_REF] Ghafari | Context-bounded translations for concurrent software: An empirical evaluation[END_REF][START_REF] La Torre | Model-checking parameterized concurrent programs using linear interfaces[END_REF]. For a more thorough comparison of these sequentializations, see Section 5.

Recently Kidd et al. [START_REF] Kidd | One stack to run them all: Reducing concurrent analysis to sequential analysis under priority scheduling[END_REF] have shown how to sequentialize priority preemptive scheduled programs, and Garg and Madhusudan [START_REF] Garg | Compositionality entails sequentializability[END_REF] have proposed an overapproximating sequentialization, albeit by exposing task-local state to other tasks. Both reductions assume a finite number of statically-declared tasks.

More generally, sequentialization could be seen as any linear traversal of the task-creation tree. The sequentializations we consider here are restricted to depth-first traversal, since they target sequential recursive programs, whose unbounded structure is, in general, contained to the procedure stack; the stackbased data-structure used for the depth-first traversal can be combined with the program's procedure stack. However, if one is willing to target other program models, one can consider other task-tree traversals, e.g., breadth-first using queues, or a completely non-deterministic traversal respecting the task-creation order, keeping, for instance, a multiset of horizon tasks. Atig et al. [START_REF] Atig | Analyzing asynchronous programs with preemption[END_REF][START_REF] Atig | Context-bounded analysis for concurrent programs with dynamic creation of threads[END_REF]'s bounded explorations of programs with dynamic task-creation, by reduction to Petri-net reachability, are sequentializable in this sense.

Our characterization of sequentializability could also be relaxed to allow the exchange of local-state valuations (or alternatively, unbounded sequences of global-state valuations) between tasks. For instance, explorations based on bounded languages [START_REF] Kahlon | Tractable dataflow analysis for concurrent programs via bounded languages[END_REF][START_REF] Ganty | Bounded underapproximations[END_REF] take this approach, essentially restricting concurrent exploration to inter-task interactions conforming to a regular pattern; then each task is executed in isolation by taking its product with the pattern-automaton. We simply note that the existing sequentializations avoid the (possibly expensive) computation of such a product.

Conclusion

We have proposed a framework for parameterized and compositional concurrent program analysis based on reduction to sequential program analysis. Our framework applies to a general class of shared-memory concurrent programs, with arbitrary preemption and dynamic task-creation, and strictly captures the known (round-based) sequentializations. It is our hope that this understanding will lead to further advances in sequential reductions, e.g., by enlightening efficiently-encodable instances of the general framework.

Though we have unified the existing sequentializations while maintaining their desirable qualities (i.e., sequential program model, compositionality, parameterization) by relaxing the global round-robin schedule, we are aware of one remaining restriction imposed by our framework. Besides the round-robin restriction imposed by the existing sequentializations, there is an implicit restriction imposed by translating task-creation directly to procedure calls: the tasks created by a single task are visited in the order they are created. Though further generalization is possible (e.g., by adding unbounded counters to the target program), such reductions will likely lead to much more complex analyses.

Reasoning in the other direction (i.e., {|P |} c ⊆ {|P |} a ) proceeds similarly, essentially showing that any successfully-stitched (via Interleave) segment sequence σ without using the NewRound rule corresponds to an asynchronous execution of the contiguous segments of σ. Proof. This is immediate, since every k-bounded compositional execution is both a (k + 1)-bounded execution, and a compositional execution. Furthermore, every compositional execution uses only finite-sized bags. 9a gives a program P in which every reachable state is reachable (with a fixed bound) in the bounded compositional semantics (by interleaving a B task at the yield point of each A task), though there is no bound such that global-round semantics express every reachable state. Note that any k global-round exploration only explores y-values less than k, since (i) every A task must be executed between two distinct rounds to increment y, and (ii) each posted A task must begin after the second round of the A task that posted it.

C The Sequential Program Statements

The compositional semantics explores every positive value j ∈ N of y with bag-sizes bounded by k = 4 (see Fig. 9b): each A task exports a pair of segment summaries-i.e., before the yield point, and after-and each B task exports a single summary. Each parent task (i.e., the one posting) saves one summary from the beginning of A (with y = i) to the yield point (with x = false, y = i), and begins a second segment from the global value x= true, y = i. In the second segment we then take the then branch, increment y, and import bags from the posted A and B tasks. From the incremented value of y (i + 1 in Fig. 9b) we apply the first segment of the posted A task, followed by the only segment of B, followed by the second A segment, ending with y = j. In this way, each A task is interrupted by a B task, and is allowed to increment y. As the number of recursive posts to A is never bounded, the value of y is incremented an arbitrary number of times.

PFig. 1 .

 1 Fig. 1. The grammar of asynchronous programs. Each program P declares a single type-T global variable g, and a sequence of procedures named p1 . . . pn ∈ Procs * . Each procedure p has single type-T parameter l, and a top-level statement (i.e., the procedure body) denoted sp. This program syntax is made simple only to simplify presentation; various extensions-e.g., to multiple global and local variables-can be encoded by varying the type T ; see Appendix A.

Post∈Fig. 2 .

 2 Fig. 2. The transition relation → a P for an asynchronous program P is given by combining the transitions above with the sequential transition relation → s P .

Fig. 3 .Fig. 4 .

 34 Fig. 3. The summary bag operations. Circles represent global valuations (double circles equivalences), and are paired together in rounded rectangle round summaries. Interfaces are drawn as stacked round summaries, and shading is used only to easily identify summaries. (a) Export a constructed interface, (b) begin a round by finalizing the current round a, b , and guessing a valuation c to begin the next, (c) import sub-task interface, (d) interleave the first unconsumed round a, b of a sub-task, updating the current global state from a to b. The round-summaries Bex to be exported appear above the dotted line, and the collection Bim of imported sub-task interfaces appears below.

Fig. 5 .

 5 Fig. 5. Simulating an asynchronous execution (a) as a compositional execution, where task A posts B and C, then is interrupted by B, then is eventually re-dispatched, and upon completion is followed directly by C, which is interrupted by B before completing. (b) The bag used to reconstruct A's interface, and (c) the constructed interface for A.

Fig. 6 .

 6 Fig. 6. The bag simplification operations: (a) merging two disconnected but contiguous round summaries a, b and b, c (resulting in (b)), and (b) merging two consecutive and contiguous summaries a, c and c, d (resulting in the small adjacent bag).

Fig. 7 .

 7 Fig. 7. (a) 3 global-round exploration, and (b) 4-delay exploration, for a program in which task A creates B and E, and task B creates C and D. Each task's interface (drawn with dashed-lines) summarizes 3 uninterrupted computations (drawn with squiggly arrows) of the task and all of its sub-tasks. Bold arrows connect global-state valuations, and dotted arrows connect local-state valuations. Note that the 3-round exploration allows each task 2 interruptions, while the 4-delay exploration allows all tasks combined only 4 interruptions.

Theorem 3 .

 3 The k global-round semantics is subsumed by the k-bounded compositional semantics, i.e., for all programs P we have {|P |} k gr {|P |} k c .

Theorem 2 .

 2 The sequence of bounded compositional semantics forms a monotonically increasing chain whose limit is identical to the compositional semantics, i.e., {|P |} 0c ⊆ {|P |} 1 c ⊆ . . . ⊆ k∈N {|P |} k c = {|P |} c .

For a statement

  context S (see Section 2), we write g, , S w, m [s] to denote the configuration g, , S[s] w, m . For convenience we also define e( g, , s, w, m ) def = e(g, ) expression evaluation g, w, m • w def = g, w w, m frame push/pop g, w, m (g ← g ) def = g , w, m global update g, , s w, m (l ← ) def = g, , s w, m local update.

Fig. 8

 8 Fig.8gives the transition relation → s P for the sequential program statements. The choice operator is used in the Call and Return-Sync rules only as a placeholder for an undetermined value. The Assume rule restricts the set of valid executions: a step is only allowed when the predicated expression e evaluates to true. (This statement-usually confined to intermediate languages-is crucial in code-to-code translations in the guess-and-constrain style sequential program reductions[START_REF] Lal | Reducing concurrent analysis under a context bound to sequential analysis[END_REF][START_REF] Emmi | Delay-bounded scheduling[END_REF].)

Fig.

  Fig.9agives a program P in which every reachable state is reachable (with a fixed bound) in the bounded compositional semantics (by interleaving a B task at the yield point of each A task), though there is no bound such that global-round semantics express every reachable state. Note that any k global-round exploration only explores y-values less than k, since (i) every A task must be executed between two distinct rounds to increment y, and (ii) each posted A task must begin after the second round of the A task that posted it.The compositional semantics explores every positive value j ∈ N of y with bag-sizes bounded by k = 4 (see Fig.9b): each A task exports a pair of segment summaries-i.e., before the yield point, and after-and each B task exports a single summary. Each parent task (i.e., the one posting) saves one summary from the beginning of A (with y = i) to the yield point (with x = false, y = i), and

Fig. 8 .

 8 Fig. 8. The transition relation → s P for the sequential statements of a program P .

See Section 4 for complexity considerations.

As our development is independent from architectural particularities, "tasks" may correspond to threads, processes, asynchronous methods, etc.

An enumerative analysis algorithm can handle "guessing" by attempting every reached global valuation; a symbolic algorithm just creates a new symbol.

Disallowing use of the NextRound rule in the top-level execution ensures that unchecked guessed global-state valuations are not considered reachable.

We consider initial configurations g, , s , ∅ and g, g, , s , B ∅ as equal.

Here the literature has assumed a fixed number of finite-state program variables in order to ignore the effect of complexity resulting from data. Indeed the reachability problem is EXPTIME-complete in the number of variables, due to the logarithmic encoding of states in the corresponding pushdown system.

Using the extension described at the end of Section 4, this combination does not require additional bag space.

Since we are interested here in analyses amenable to sequentialization, we consider only the depth-first delay-bounded task-scheduler[START_REF] Emmi | Delay-bounded scheduling[END_REF].

A Syntactic Sugar

The following syntactic extensions are reducible to the original syntax of asynchronous programs of Section 2. Here we freely assume the existence of various type-and expression-constructors. This does not present a problem since our program semantics does not restrict the language of types nor expressions.

Multiple types. Multiple type labels T 1 , . . . , T j can be encoded by systematically replacing each T i with the sum-type T = j i=1 T i . This allows local and global variables with distinct types.

Multiple variables. Additional variables x 1 : T 1 , . . . , x j : T j can be encoded with a single record-typed variable x : T , where T is the record type { {f 1 : T 1 , . . . , f j : T j } }, and all occurrences of x i are replaced by x.f i . When combined with the extension allowing multiple types, this allows each procedure to declare any number and type of local variable parameters, distinct from the number and type of global variables.

Local variable declarations. Additional (non-parameter) local variable declarations var l : T to a procedure p can be encoded by adding l to the list of parameters, and systematically adding an initialization expression (e.g., the choice expression , or false) to the corresponding position in the list of arguments at each call site of p to ensure that l begins correctly (un)initialized.

Unused values. Call assignments call x := p e, where x is not subsequently used, can be written as call _ := p e, where _:T is an additional unread local variable, or simpler yet as call p e.

Let bindings. Let bindings of the form let x: T = e in can be encoded by declaring x as a local variable var x: T , immediately followed by an assignment x := e. This construct is used to explicate that the value of x remains constant once initialized. The binding let x: T in is encoded by the binding let x: T = in, where is the choice expression.

Tuples. Assignments (x 1 , . . . , x j ) := e to a tuple of variables x 1 , . . . , x j are encoded by the sequence let r : { {f 1 : T 1 , . . . , f j :

where r is a fresh variable, and s[e 1 /e 2 ] replaces all occurrences of e 2 in s with e 1 . When a tuple-element x i on the left-hand side of an assignment is unneeded (e.g., from the return value of a call ), we may replace the occurrence of x i with the variable-see the "unused values" desugaring.

Arrays. Finite T j -arrays with j elements of type T can be encoded as records of type T = { {f 1 : T, . . . , f j : T } }, where f 1 , . . . , f j are fresh names. Occurrences of terms a[i] are replaced by a.f i , and array-expressions [e 1 , . . . , e j ] are replaced by record-expressions { {f 1 = e 1 , . . . , f j = e j } }.

B Proofs of Theorems

We show by induction on the sub-task relation how to construct a complete task-segment sequence σ u0 corresponding to the execution h starting from an initial task u 0 . For u ∈ TaskIDs, we define h u as the sub-sequence of h containing only configurations of u and u's (transitive) sub-tasks. As the basis, when u 0 does not post any additional tasks, then the total order on segments of task u 0 defined by h u0 is easily replicated in the compositional semantics, using the NextRound rule into a segment sequence σ u0 .

Given two words σ, τ ∈ Σ * of some alphabet Σ, the shuffle of σ and τ , denoted σ τ , is the set of words σ 1 τ 1 σ 2 τ 2 . . . ∈ Σ * such that σ = σ 1 σ 2 . . . and τ = τ 1 τ 2 . . .. The shuffle of a sequence of words is obviously defined, given that is commutative and associative. When u 0 posts tasks u 1 , . . . , u i , the inductive hypothesis defines for each h uj a segment sequence σ uj . As h u0 is given by some shuffling of h u1 , . . . , h ui with the segments of task u 0 (respecting the segment causality relation <), we must construct a segment sequence σ u0 given by an arbitrary shuffling of σ u1 , . . . , σ ui -given by the SubTask rule-with the segments of task u 0 (again, respecting the segment causality relation <). It is not hard to verify that using the Interleave, NextRound, and Resume rules, the compositional semantics does indeed consider every such shuffling, sequencing each segment one at a time into an exported total order; for each segment taken from a sub-task (given by the SubTask rule), the compositional execution begins a new round (via NextRound), and consumes the given segment (via Interleave); for each segment of the current task, the compositional execution simply begins a new round, and applies a sequence of sequential rules. The causality relation < is never violated, since a sub-task's segments cannot be sequenced until they are provided by a corresponding SubTask rule, and segments of the same task are sequenced in their causal order.

In the initial task u 0 , the compositional execution behaves similarly, except does not apply the NextRound rule. Since h is a valid asynchronous execution, the segments of σ u0 are contiguous-i.e., the global valuation reached by each segment is equal to the initial global valuation of the next. Thus the Interleave rule can be repeatedly applied, stitching together the contiguous segments, building a complete compositional execution from σ u0 .