Affordable Access

Publisher Website

Verification of Fine-grain Concurrent Programs

Authors
Journal
Electronic Notes in Theoretical Computer Science
1571-0661
Publisher
Elsevier
Publication Date
Volume
209
Identifiers
DOI: 10.1016/j.entcs.2008.04.010
Keywords
  • Fine-Grain Concurrent Programs
  • Flowcharts
  • Floyd Assertions
  • Petri Nets
Disciplines
  • Computer Science
  • Design
  • Mathematics

Abstract

Abstract 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.

There are no comments yet on this publication. Be the first to share your thoughts.