On execution spaces of PV-programs

TL;DR

This paper formalizes PV-programs using semaphores, analyzing their execution spaces, and proves that any finite homotopy type can be realized as a connected component of such spaces.

Contribution

It provides a formal framework for PV-programs and demonstrates the universality of their execution space topology in representing finite homotopy types.

Findings

Every finite homotopy type can appear as a connected component of a PV-program's execution space.

Provides a formal definition of PV-programs and their state and execution spaces.

Establishes the topological richness of PV-program execution spaces.

Abstract

Semaphores were introduced by Dijkstra as a tool for modeling concurrency in computer programs. In this paper we provide a formal definition of PV-programs, i.e. programs using semaphores, their state spaces and execution spaces. The main goal of this paper is to prove that every finite homotopy type may appear as a connected component of the execution space of a PV-program.