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 denoting writing on a memory location, and followed by a denoting reliquinshing memory location once writing is finished.
The interleaving semantics (all possible scenarii of execution) is very large.
and share two integers and . adds to and multiplies by . adds to and multiplies by . 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 and 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.
Dipaths are continuous increasing paths. A dihomotopy is a homotopy through dipaths.
Definition 1 The trace space is the space of dipaths from to 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, is a cube with a number of subcubes removed.
Idea: extend a removed subcube in a direction, e.g. into , and look wether there a exists a dipaths joining to outside it.
Code blocking holes by Boolean matrices. Say a matrix is dead (resp. alive) wether a connecting dipath exists or not. The set (resp. ) of dead (resp. alive) matrices are posets (for the entrywise ordering).
Theorem 2 determines which, in turn, fully determines the homotopy type of the thrace space .
This follows from the following facts.
Proposition 3 , is not .
Proposition 4 Schedules are is -correspondence with connected components of , where two matrices are connected if there entrywise contains no null row.
In other words, from the data of , define an hypergraph structure on . Then 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 -simplex for each row, where is the number of ‘s in the row.
There is a variant for randomized programs.