Geometric methods have been used for 20 years to prove impossibility results for fault-tolerant concurrent computing. We study these methods from a semantical perspective: in what sense do they constitute a semantics for concurrent programs?

In this talk, I will explain how to derive these geometric models from a concrete operational semantics based on interleavings of execution traces. To do so, I will review and compare different trace-based methods for specifying behaviors of concurrent objects.