Automatic Synthesis of Diffusing Computation Using Pre-synthesized Detectors/Correctors

Problem specification:

We present a case study of automatic addition of fault-tolerance to distributed programs using presynthesized distributed components. Specifically, we extend the scope of automatic addition of fault-tolerance using presynthesized components to the case where we automatically add hierarchical components to fault-intolerant programs, whereas in our previous work, we have shown the addition of linear presynthesized components to programs. Also, our case study provides an example for the cases where multiple components are simultaneously added to a program. Towards this end, we present an automatically generated diffusing computation program that provides nonmasking fault-tolerance -- where, in the presence of faults, the nonmasking program guarantees recovery to states from where it satisfies its safety and liveness specifications. Since presynthesized components provide reuse in the synthesis of fault-tolerant distributed programs, we expect that our method will pave the way for automatic addition of fault-tolerance to large-scale programs.

The input text file to our synthesis framework.

The intermediate program synthesized with FTSyn (includes high atomicity recovery actions).

The composition of the program and presynthesized components in Promela modeling language.