LIMITATIONS AND CAPABILITIES OF WEAK MEMORY CONSISTENCY SYSTEMS
Date
2000-03-22
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
This dissertation develops and exploits a formalism for specifying
memory consistency models. This formalism lays down the foundations for
describing memory consistency models at various levels, and develops techniques
to prove the equivalence between models defined at different levels. Two
levels, called non-operational and operational, are addressed in this
dissertation. The non-operational level describes these models in terms of
program instructions or procedures, while the operational level describes them
in terms of implementation events. Formal techniques are developed to prove
the equivalence of rigorous specifications at both levels. This formalism is
then exploited to define the memory consistency models of two state-of-the-art
multiprocess systems: the SPARC version 8 architecture and the Java Virtual
Machine. These models are defined at both operational and non-operational
levels. These operational and non-operational descriptions are proved
equivalent. The SPARC models provide "reasonably" weak memory consistency
models that are capable of avoiding the use of explicit synchronization
primitives for certain problems. However, Java provides a consistency model
that is completely dependent on synchronization primitives, without which no
form of coordination between different threads is possible. Fundamental
process coordination problems have been extensively studied for traditional
systems with strong memory consistency. This dissertation revisits the
critical section and the producer/consumer problems in the context of weak
memory consistency models. It establishes that the majority of known weak
memory consistency models are incapable of supporting a solution to the
critical section problem without the use of explicit synchronization
primitives. Surprisingly, most of these models are capable of supporting
solutions to versions of the producer/consumer problem without the use of these
primitives.
Description
Keywords
Computer Science