Date of Award

4-23-2019

Document Type

Thesis

Degree Name

Master of Science (MS)

Department

Computer Science

First Advisor

Peiyi Tang

Abstract

This experiment attempted to push the limits of the TLA+ specification language and TLC model checker by specifying and checking a modern, set associative, write back caching system. This was done through the writing of a specification that focused on the operation of a single level, multi-CPU cache. While a fully associative and direct mapped version of the specification eventually model checked in a reasonable amount of time, the added complexity of a fully associative cache proved too much for an 80 processor high performance machine with almost 1TB of hard drive space. The use of a simulation mode allowed us to feasibly test the fully associative cache sufficiently to allow confidence in its correctness.

Download

Share

COinS