Sleptsov Net Virtual Machine Implementation on GPU
摘要
Sleptsov Net Computing (SNC) provides a vivid graphical language, fine granulation of concurrent processes, and wide application of formal methods for reliable software design. We are interested in the minimal time complexity for reaching a terminal state of a given net. Computing memory implementation of dedicated SNC hardware promises hyper-performance. At present, we have achieved reasonable performance enhancements on conventional multicore CPUs and GPUs. Classical nondeterministic transition choice for Petri and other place-transition nets, Sleptsov nets, in particular, is time-consuming, representing a bottleneck, especially for GPU implementations. Here we present a novel approach to fast fireable transition choice within a net extended with priority arcs. We compose a lattice of transitions concerning the priority relation and reorder transitions layer by layer, in any order for a layer. As proven in SNC papers, the result of computations is invariant concerning any valid transition sequence choice. We demonstrate that the first fireable transition choice on reordered transitions constructs a valid sequence of fireable transitions. Results of the step complexity evaluations agree with the obtained benchmarks and yield 2–4 times the speed-up of computations. Some other improvements have been made to reduce the number of required GPU threads and memory, based on sparse matrix representation.