Verification of Fine-grain Concurrent Programs

Intel has announced that in future each standard computer chip will contain many processors operating concurrently on the same shared memory; their use of memory is interleaved at the fine granularity of individual memory accesses. The speed of the individual processors will never be significantly faster than they are today. Continued increase in performance will therefore depend on the skill of programmers in exploiting the concurrency of this multi-core architecture. In addition, programmers will have to avoid increased risks of race conditions, non-determinism, deadlocks and livelocks. To reduce these risks, we propose a theory of correctness for fine-grain concurrent programs. The approach is just an amalgamation of a number of well-known and well-researched ideas, including flowcharts, Floyd assertions, Petri nets, process algebra, separation logic, critical regions and rely/guarantee reasoning. These ideas are applied in combination to the design of a structured calculus of correctness for fine-grain concurrent programs; it includes the main features of a structured concurrent programming language.