Document Type

Technical Report

Publication Date

2007

Subjects

Cache memory, Systems software, Memory management (Computer science), Symbolic and mathematical logic, Formal methods (Computer science)

Abstract

We verify some correctness properties of the DASH cache coherence protocol using Ωmega. Ωmega is a language with a rich type system featuring GADTs, type functions, and user-guided type checking rules. Cache coherence protocols have both safety properties and liveness properties. We show how to describe some of the safety properties of DASH cache coherence protocol in mega. Since liveness properties are not easily expressed by types, we investigate invariants sufficient to imply some of the liveness properties of concern, and assert those invariants as well in the type system of Ωmega. Using Ωmega, we can have both a working program and an automatically checked proof of its properties because Ωmega is both a programming language and a logic. Tightly coupled programs and their properties using types guides us both in the construction of the program and in strategies for modification that preserves the essential properties.

Description

This technical report is based on the paper submitted to the 2007 Spring Research Proficiency Examination of Computer Science Department at Portland State University.

Portland State University Computer Science Department Technical Report #08-02, 2007.

Persistent Identifier

https://archives.pdx.edu/ds/psu/30741

Download

Share

COinS