Cache coherence is an integral part of shared-memory systems but is also widely considered to be one of the most complex parts of such systems. Much prior work has addressed this complexity and the verification techniques to prove the correctness of hardware coherence. Given the new multicore era with increasing number of cores, there is a renewed debate about whether the complexity of hardware coherence has been tamed or whether it should be abandoned in favor of software coherence. This article revisits the complexity of hardware cache coherence by verifying a publicly available, state-of-the-art implementation of the widely used MESI protocol, using the Murφ model checking tool. To our surprise, we found six bugs in this protocol, most of which were hard to analyze and took several days to fix. To compare the complexity, we also verified the recently proposed DeNovo protocol, which exploits disciplined software programming models. We found three relatively easy to fix bugs in this less mature protocol. After fixing these bugs, our verification experiments showed that, compared to DeNovo, MESI had 15X more reachable states leading to a 20X increase in verification (model checking) time. Although we were eventually successful in verifying the protocols, the tool required making several simplifying assumptions (e.g., two cores, one address). Our results have several implications: (1) they indicate that hardware coherence protocols remain complex; (2) they reinforce the need for protocol designers to embrace formal verification tools to demonstrate correctness of new protocols and extensions; (3) they reinforce the need for formal verification tools that are both scalable and usable by non-expert; and (4) they show that a system based on hardware-software co-design can offer a simpler approach for cache coherence, thus reducing the overall verification effort and allowing verification of more detailed models and protocol extensions that are otherwise limited by computing resources.

For parallelism to become tractable for mass programmers, shared-memory languages and environments must evolve to enforce disciplined practices that ban "wild shared-memory behaviors;'' e.g., unstructured parallelism, arbitrary data races, and ubiquitous non-determinism. This software evolution is a rare opportunity for hardware designers to rethink hardware from the ground up to exploit opportunities exposed by such disciplined software models. Such a co-designed effort is more likely to achieve many-core scalability than a software-oblivious hardware evolution. This paper presents DeNovo, a hardware architecture motivated by these observations. We show how a disciplined parallel programming model greatly simplifies cache coherence and consistency, while enabling a more efficient communication and cache architecture. The DeNovo coherence protocol is simple because it eliminates transient states - verification using model checking shows 15X fewer reachable states than a state-of-the-art implementation of the conventional MESI protocol. The DeNovo protocol is also more extensible. Adding two sophisticated optimizations, flexible communication granularity and direct cache-to-cache transfers, did not introduce additional protocol states (unlike MESI). Finally, DeNovo shows better cache hit rates and network traffic, translating to better performance and energy. Overall, a disciplined shared-memory programming model allows DeNovo to seamlessly integrate message passing-like interactions within a global address space for improved design complexity, performance, and efficiency.

We illustrate how to employ metacircular assume/guarantee reasoning to reduce the verification complexity of finite instances of protocols for safety, using nothing more than an explicit state model checker. The formal underpinnings of our method are based on establishing a simulation relation between the given protocol M, and several overapproximations thereof, Mtilde1,..., Mtildek. Each Mtildeisimulates M, and represents one "view" of it. The Mtildeis depend on each other both to define the abstractions as well as to justify them. We show that in case of our hierarchical coherence protocol, its designer could easily construct each of the Mtildeiin a counterexample guided manner. This approach is practical, considerably reduces the verification complexity, and has been successfully applied to a complex hierarchical multicore cache coherence protocol which could not be verified through traditional model checking

The only practical way to verify the correctness of distributed algorithms with a high degree of confidence is to construct machine-checked, formal correctness proofs. In this paper we explain how to do so using HOL – an interactive proof assistant for higher-order logic develop by Gordon and others. First, we describe how to build an infrastructure in HOL that supports reasoning about distributed algorithms, including formal theories of predicates, temporal logic, labeled transition systems, simulation of programs, translation of properties, and graphs. Then we demonstrate, via an example, how to use the powerful intuition about events and causality to guide and structure correctness proofs of distributed algorithms. The example used is the verification of PIF (propagation of information with feedback), which is a simple but typical distributed algorithm due to Segall.

An efficient way to synchronize an asynchronous network with a bounded delay message delivery is presented. Two types of synchronization algorithm are presented. Both types require an initializing phase that costs mod E mod messages (where mod E mod is the number of links). The first requires an additional bit in every message and increases the time complexity by a factor of 2. The second does not require any additional bits but increases the time complexity by a factor of 3. How to overcome differences in nodal timer rates is explained.>

Designers of autonomous distributed algorithms ( i.e., algorithms whose complete input is available before the start of execution) customarily refer to temporal ordering in describing the behavior of their algorithms-statements like "after A, task B is performed."In the absence of an explicit termination detection for A built into the algorithm such a statement should be puzzling.However, the available proof methodologies do not seem to hinge on such statements.This paper provides firm theoretical ground for such as-