Synthesis of Large Dynamic Concurrent Programs from Dynamic Specifications
| dc.creator | Attie, Paul C. | |
| dc.date | 2008-01-10 | |
| dc.date.accessioned | 2026-07-07T08:53:46Z | |
| dc.date.available | 2026-07-07T08:53:46Z | |
| dc.description | We present a tractable method for synthesizing arbitrarily large concurrent programs, for a shared memory model with common hardware-available primitives such as atomic registers, compare-and-swap, load-linked/store conditional, etc. The programs we synthesize are dynamic: new processes can be created and added at run-time, and so our programs are not finite-state, in general. Nevertheless, we successfully exploit automatic synthesis and model-checking methods based on propositional temporal logic. Our method is algorithmically efficient, with complexity polynomial in the number of component processes (of the program) that are ``alive'' at any time. Our method does not explicitly construct the automata-theoretic product of all processes that are alive, thereby avoiding \intr{state explosion}. Instead, for each pair of processes which interact, our method constructs an automata-theoretic product (\intr{pair-machine}) which embodies all the possible interactions of these two processes. From each pair-machine, we can synthesize a correct \intr{pair-program} which coordinates the two involved processes as needed. We allow such pair-programs to be added dynamically at run-time. They are then ``composed conjunctively'' with the currently alive pair-programs to re-synthesize the program as it results after addition of the new pair-program. We are thus able to add new behaviors, which result in new properties being satisfied, at run-time. We establish a ``large model'' theorem which shows that the synthesized large program inherits correctness properties from the pair-programs. | |
| dc.description | 46 pages | |
| dc.identifier | https://arxiv.org/abs/0801.1687 | |
| dc.identifier | http://arxiv.org/abs/0801.1687 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/145737 | |
| dc.subject | Logic in Computer Science | |
| dc.title | Synthesis of Large Dynamic Concurrent Programs from Dynamic Specifications | |
| dc.type | text |