From Concurrent Multi-clock Programs to Deterministic Asynchronous Implementations

摘要

We propose a general method to characterize and synthesize correctness-preserving asynchronous wrappers for synchronous processes on a globally asynchronous locally synchronous (GALS) architecture. While a synchronous process may rely on the absence of a signal to trigger a reaction, sensing absence in an asynchronous environment may be unfeasible due to uncontrolled communication latencies. A simple and common solution is to systematically encode and send absence notifications, but it is unduly expensive at run-time. Instead, our approach is based on the theory of weakly endochronous systems, which defines the largest sub-class of synchronous systems where (possibly concurrent) asynchronous evaluation is faithful to the original (synchronous) specification. Our method considers synchronous processes or modules that are specified by synchronization constraints expressed in a high-level multi-clock synchronous reactive formalism. The algorithm uses a compact representation of the abstract synchronization configurations of the analyzed process and determines a minimal set of synchronization patterns generating by union all its possible reactions. A specification is weakly endochronous if and only if these generators do not need explicit absence information. In this case, the set of generators can directly be used to synthesize the concurrent asynchronous multi-rate wrapper of the process.