Notes of Eric Goubault’s lecture

This talk belongs in the CEMPI inaugural conference, Lille, september 24-29th, 2012. It starts the Graphs and groups workshop inside that conference.

Geometry of trace spaces

This is a connection between theoretical computer science and algebraic topology. Application to static analysis of programs. I will provide a rush tour of static analysis

1. Static analysis

Want to prove some form of correctness of a program. – invariants: e.g. no division by zero. – liveness propeeties: e.g., will terminate or will deadlock.

Classically, one step in the study is interleaving semantics. We want to improve this step.

One views the program as a discrete dynamical system. Invariants correspond to first integrals. Variants (e.g. something decreases) are useful too.

1.1. Concurrent programs

We restrict to the subcase of concurrent programming. In out model, a memory is shared, processors communicate by writing and reading in it. Non sequential: need for synchronizations, and therefore, of locks granted by the memory. Every instruction is preceded by a {P} denoting writing on a memory location, and followed by a {V} denoting reliquinshing memory location once writing is finished.

The interleaving semantics (all possible scenarii of execution) is very large.

1.2. Example

{T_1} and {T_2} share two integers {a} and {b}. {T_1} adds {1} to {a} and multiplies {b} by {2}. {T_2} adds {1} to {b} and multiplies {a} by {3}. Only two memory locations. This makes 6 instructions for each. Scenarii correspond to pairs of shuffles of 6-cards packs. I.e. increasing paths (dipaths) in the product of two finite graphs. The synchronization pattern forbids certain pairs (where both {T_1} and {T_2} would have a lock on the memory).

Consider dihomotopy classes of paths. They correspond to scenarii sharing the same synchronization patterns. This (quotient) space is much smaller than the full space of paths. We want to design verification programs which need deal with dihomotopy classes only.

1.3. Geometric models

We need a variant of algebraic topology, directed algebraic topology, to take into account time.

Spaces are topological and partially ordered (in example above, X is a product with product partial order, i.e.

\displaystyle  \begin{array}{rcl}  (s,t)\leq(s',t') \Leftrightarrow s\leq t \textrm{ and } s'\leq t'). \end{array}

Dipaths are continuous increasing paths. A dihomotopy is a homotopy through dipaths.

Definition 1 The trace space {T(X)(b,e)} is the space of dipaths from {b} to {e} up to increasing reparametrizations.

A schedule is a dihomotopy class of dipaths with fixed endpoints.

In other words, we wish to study the connected components, and, more generally, the homotopy types of trace spaces. These spaces are homotopy equivalent to certain prodsimplicial compexes which can be calculated combinatorially. Typically, {X} is a cube with a number of subcubes removed.

2. Results

2.1. Method

Idea: extend a removed subcube {(s,t)\times(s',t')} in a direction, e.g. into {(s,t)\times(s_b,t')}, and look wether there a exists a dipaths joining {b} to {e} outside it.

Code blocking holes by Boolean matrices. Say a matrix is dead (resp. alive) wether a connecting dipath exists or not. The set {D} (resp. {C}) of dead (resp. alive) matrices are posets (for the entrywise ordering).

Theorem 2 {D} determines {C} which, in turn, fully determines the homotopy type of the thrace space {T(X)(b,e)}.

This follows from the following facts.

Proposition 3 {M\in C} {\Leftrightarrow} {\forall N\in D}, {N} is not {\leq M}.

Proposition 4 Schedules are is {1-1}-correspondence with connected components of {C}, where two matrices are connected if there entrywise {\min} contains no null row.

2.2. Combinatorics

In other words, from the data of {D}, define an hypergraph structure on {X\times X}. Then {C} is the set of minimal transversals.

2.3. The prodsimplicial structure

A prodsimplicial set is a space made up of simplices and products of simplices, glued along their faces.

Here, each Boolean matrix is associated with a prodsimplex: a product of a {k-1}-simplex for each row, where {k} is the number of {1}‘s in the row.

3. Conclusion

There is a variant for randomized programs.

Advertisements

About metric2011

metric2011 is a program of Centre Emile Borel, an activity of Institut Henri Poincaré, 11 rue Pierre et Marie Curie, 75005 Paris, France. See http://www.math.ens.fr/metric2011/
This entry was posted in Workshop lecture and tagged . Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s