Quantitative Synthesis for Concurrent Programs
The authors present an algorithmic method for the quantitative, performance-aware synthesis of concurrent programs. The input consists of a non-deterministic partial program and of a parametric performance model. The non-determinism allows the programmer to omit which (if any) synchronization construct is used at a particular program location. The performance model, specified as a weighted automaton, can capture system architectures by assigning different costs to actions such as locking, context switching, and memory and cache accesses. The quantitative synthesis problem is to automatically resolve the non-determinism of the partial program so that both correctness is guaranteed and performance is optimal.