Synthesis and analysis for concurrent programs (Syncopia)

A strong persisting trend in computer and software systems is the omni-presence of distributed and concurrent systems, as witnessed by multi-core architectures, networks and multiprocessor systems on chip, cloud computing, IoT, smartdust, blockchain, etc. The speed at which these innovations take place bears the risk that we lose control of the reliability and predictability of the software fabric on which our world increasingly depends. The increasing degree of concurrency introduces new dimensions of complexity when it comes to guarantee the safety, security and functional correctness, creating non-determinism and tangled synchronisation problems that are extremely difficult to deal with. Qualitative synchronisation problems involve deadlock, livelock, priority inversion, data inconsistency or security attacks. Quantitative synchronisation problems concern violation of realtime deadlines, bottlenecks of throughput and utility or set up latencies. Traditional testing and exploratory debugging methods cannot cope with synchronisation problems. Therefore, in our view, it is of paramount importance to give more emphasis to the formal verification, analysis, and synthesis of concurrency aspects in the practical software development process. This project combines recent work on weak memory models and static type-checking for memory-safe multi-threaded programming with recent advances in the SP technology. This will produce a first uniform methodology for ensuring memory safety and determinacy for general abstract data types. This advances the state of the art on both sides: It will support more powerful data abstraction, where main-stream concurrent programming typically only permits primitive memory registers. It will support genuinely concurrent execution models and the consideration of weak-memory models, where SP compilers typically only generate sequential C code and ignore data races in the instruction set architecture.