CS6410: Specification Mini-project

Overview

This exercise will help you to gain experience in writing a specification for a system, component, or protocol. In class we illustrated a system specification in terms of

• allowed high-level transitions over some state space,
• an implementation described in terms of low-level transitions over some other state space, and
• use of a refinement mapping to establish the correspondence between system executions (sequences of low-level transitions) and what is allowed (sequences of high-level transitions).

This is not intended to be an exercise in fighting with formalism or mathematics. Try to strike a balance between giving informal descriptions and being completely rigorous. The chain replication paper is a good model. And since we are concerned here more with form than with function, pick a relatively simple protocol or system. For those unsure of what to choose, here are some examples that should be well suited for this assignment:

• RAID Disk Storage. The operations are read and write. This is used in the Zebra file system paper.
• Quorum Data Storage. The operations are read and write, where each operation involves a quorum of copies. Two particularly simple schemes are discussed in Gifford's paper and Herlihy's paper. Pick only one and specify that.
• Agreement. The signed message algorithm (SM) described in the Byzantine Agreement paper we are reading this semester.

What to Hand In

Section 1: Introduction

Give an informal account of what system or protocol you are specifying, including a citation to the source.

Section 2: High Level Specification

Define a high-level state space by introducing some variables and giving a type to each. Indicate which state is externally visible. Identify a set of externally visible operations (i.e., the functionality you are specifying). Then, for each externally visible operation, give a transition that models the operation. Each transition is defined by enumerating (i) a set of conditions that must hold for the transition to occur and (ii) a set of high-level state changes (i.e., assignment statements) that signify the transition has occurred. The conditions and state changes must involve only the high-level state and user-provided parameters to the operation.

Section 3: Low Level Specification (aka Implementation)

Define the low-level state space by declaring variables that the implementation actually uses. Then give the implementation of each high-level operation in terms of a sequence of transitions involving this low-level state space. As above, a transition is defined by giving a condition that will be awaited followed by some state changes (but now to the low-level state space) .

Section 4: Refinement Mapping

Give the rules (i.e., the refinement mapping) to determine the high-level state that corresponds to each given low-level state. Externally visible high-level variables should correspond to low-level variables with no transformation; other high-level variables can be given values that is any function of any subset of the low-level variables. Then, for each low-level state transition that occurs while a low-level operation is executing, show: (i) what is the corresponding high-level state at the start and end of the low-level transition, and (ii) that the high-level transition resulting from this low-level operation is either a "stutter step" of the high-level state or is allowed by one of the high-level transitions given in Section 1.

We will only grade typeset documents. Latex is probably easier to use for mathematical notation than word. Five or six pages should suffice for specifying the kinds of simple protocols suggested above.