A conditionally optimal algorithm for deciding whether basic parallel systems are safe

What is it about?

An important question in the study of any computation system is: "can the system enter an unsafe configuration?". Let's consider a simplified model of a general computer with many programs running in parallel. One should think that the parallel programs are discrete units that can be in any of the four locations; for example, it could be the case that there are some 30 programs reading from the hard drive, 70 programs waiting for a data from an open socket, 500 programs are currently not loaded (and are stored on the hard drive), and 6 programs executing on the processor. For the sake of this example, we shall make the simplifying assumption that the computer has an eight-core processor and if ever at least nine programs are executing on the processor, then this causes a fault and the computer shuts down. The computer will have many different instructions scheduling programs to load, unload, read from the hard drive, and wait for data from a socket. Given such a computer system, we can now ask the aforementioned safety question: can it ever reach an unsafe configuration? In this case, an unsafe configuration is one in which there are at least nine programs in the processor. To this end, we study a model of computation called vector addition systems with states (VASS) which are an equivalent model of computation to Petri nets. These models were first defined in the 1960s as modest, yet robust, models of computation for studying parallel systems. More precisely, a VASS can be seen a directed graph whose edges are labelled with integer vectors. The VASS has counters that can only store nonnegative integer values. Accordingly, a configuration of a VASS consists of a node (where you are in the directed graph) and a vector of natural numbers (the current counter values). From a given configuration, a VASS can transition to another configuration by traversing an edge in the graph so long as adding the edge's vector does not make any of the counters negative. In full generality, the problem of reaching unsafe configurations is called coverability. As input, one specifies a VASS, an initial configuration, and some target configuration and the coverability problem asks whether there is a run (a sequence of configurations) from the initial configuration to some final configuration which is at the same node as the target configuration but perhaps with greater counter values. In our paper, we present an algorithm for deciding coverability in VASS. Our algorithm improves on the seminal work of Rackoff (1978) but reuses much of his approach. To see the improvement, we must define some terms. Let n represent the size of the VASS (i.e. the number of nodes in the graph plus the size of all the vectors on the edges of the graph). Let d be the number of counters that the VASS manipulates (that is also the dimension of all the vectors on the edges of the graph). Roughly speaking, Rackoff argued that if there is a run to some final covering configuration, then there must be a covering run of length at most n^(d^d). This yields two algorithms. One that runs in double-exponential time, precisely the algorithm will terminate after approximately n^(d^d) steps. The other runs in exponential spare, precisely the algorithm only requires approximately (d^d)*log(n) space. Our new algorithm for coverability in VASS relies on an improved bound on the minimal length of covering runs. We improve on Rackoff's bound by arguing that if there is a run to some final covering configuration, then there is a covering run of length at most n^(2^d). Accordingly, this yields two algorithms: one that requires approximately n^(2^d) time, and the other that requires (2^d)*log(n) space.

Featured Image

Photo by ian kelsall on Unsplash

Photo by ian kelsall on Unsplash

Why is it important?

This paper is important for two main reasons. First, it improves on a widely used algorithm for analysing parallel computation systems. Second is that this improvement is (conditionally) optimal. To support the first point, coverability is often used in tools and benchmarks for deciding safety and liveness in Petri nets/VASS. Also, improving Rackoff's algorithm for coverability was also asked as an open problem in a well-known and well-cited paper by Mayr and Meyer (1981). Further details can be found in the first second of the paper. To support the second point, we prove a lower bounds that heavily suggests that our algorithms are essentially optimal. First, two years prior to Rackoff's paper, Lipton (1976) proved that deciding coverability in VASS required (2^d)*log(n) space. This means that our second algorithm, terminating using approximately (2^d)*log(n) space is essentially unconditionally optimal. Furthermore, in our new paper, we prove that if one is to assume the Exponential Time Hypothesis, then there does not exist any algorithm for coverability that terminates in less than n^(2^(d/4)) steps. This means that our other algorithm that terminates in approximately n^(2^d) steps is almost conditionally optimal. Further substantial improvements to coverability in VASS would imply substantial improvements to extremely well-studied problems like satisfiability, graph colouring, and subset sum.