ORIGINAL

Abstract

Even as most of today's computer systems have turned to parallelism to improve performance, important challenges still need to be addressed.

In Part A, we observe that documentation often remains informal, incomplete or even incorrect regarding the memory consistency models of parallel systems, leading to programmer and designer confusion and bugs. Existing tools for empirical memory consistency testing use large numbers of iterations of simple multi-threaded litmus tests, typically employing thread synchronization at every iteration. This synchronization imposes a significant overhead, reducing testing performance and efficiency. We propose new litmus test variants called perpetual litmus tests, which allow for more efficient consistency testing, using arithmetic sequences to reduce the required synchronization points. We present PerpLE, a software suite for the generation, execution, and analysis of perpetual litmus tests. We introduce an algorithm for determining the outcomes of perpetual litmus tests as well as a scalable linear heuristic algorithm. We evaluate PerpLE against litmus7 on an x86 system. Our tool exposes a wider variety of outcomes while being faster than all litmus7 synchronization modes (8.89x faster than the default user mode), while the detection rate of outcomes of interest is increased by over two orders of magnitude.

In Part B, we verify the Decoupled Consumer-Producer (DCP) subsystem of the Intelligent Storage (IS) tiles in the DECADES architecture. In order to exhaustively verify DCP despite its complexity, we turn to formal verification, which we perform bottom-up in three phases. Based on the system specification, we write properties in the SVA language and use JasperGold, a formal verification tool, to mathematically prove that our design never violates them. Having completely verified a single-FIFO version of our design, we are now in Phase II of verifying the current multi-FIFO version, where we have unbounded proofs for 78% of properties and bounded proofs of between 18 and 32 cycles for the rest. JasperGold also finds 100% of our code to be reachable and all finalized code (90% of the total code) to be explicitly tested by at least one property.