The alternator

摘要

An alternator is an array of interacting processes that satisfy three conditions. First, if a process has an enabled action at some state, then no neighbor of that process has an enabled action at the same state. Second, along any concurrent execution, each action is executed infinitely often. Third, along any maximally concurrent execution, the alternator is stabilizing to states where the number of enabled actions is maximal. In this paper, we specify an alternator with arbitrary topology and verify its correctness. We also show that this alternator can be used in transforming any system that is stabilizing assuming serial execution, to one that is stabilizing assuming concurrent execution.