Unformatted text preview:

Handout 6 1Massachusetts Institute of TechnologyDepartment of Electrical Engineering and Computer Science6.826 — Principles of Computer SystemsHandout 6 February 9, 1997____________________________________________________________________________Abstraction Functions and InvariantsThis handout describes the main techniques used to prove correctness of state machines:abstraction functions and invariant assertions. We demonstrate the use of these techniques forsome of the examples from handout 5.Throughout this handout, we consider modules all of whose externally invocable procedures areAPROCs. We assume that the body of each such procedure is executed all at once. Also, we do notconsider procedures that modify global variables declared outside the module underconsideration.Modules as state machinesOur methods apply to an arbitrary state machine or automaton. In this course, however, we use aSpec module to define a state machine. Each state of the automaton designates values for all thevariables declared in the module. The initial states of the automaton consist of initial valuesassigned to all the module’s variables by the Spec code. The transitions of the automatoncorrespond to the invocations of APROCs together with their result values.An execution fragment of a state machine is a sequence of the form s0, π1, s1, π2, …, where eachs is a state, each π is a label for a transition (an invocation of a procedure body), and eachconsecutive (si, πi+1, si+1) triple follows the rules specified by the Spec code. (We do not definethese rules here—wait for the lecture on formal semantics.) An execution is an executionfragment that begins in an initial state.Figure 1 shows some of the states and transitions of the state machine for the SimpleMemorymodule, and Figure 2 does likewise for the WBCache module. The arrow for each transition islabeled by the procedure name, arguments, and result.External behaviorUsually, a client of a module is not interested in all aspects of its execution, but only in somekind of external behavior. Here, we formalize the external behavior as a set of traces. That is,from an execution (or execution fragment) of a module, we extract the trace, which is thesequence of invocations of exported routines that occur in the execution (or fragment). Then theexternal behavior of the module is the set of traces that are obtained from all of its executions.Handout 6 2bcabbaabaaaabaacacWrite(2,a)Init(Read(2),a)Init(Read(3),a) (Read(1),b)(Read(1),b)Reset(a) Reset(a)Write(4,c)Figure 1: Part of the SimpleMemory state machine abbaab a abcaca Write(2,a)Init(Read(2),a)Init(Read(1),b)Reset(a)Reset(a)Write(4,c)bccab bbcaabaababacReset(a) a cbcabbc aa ba bcacbaacb a (Read(3),a)(Read(1),b)Figure 2: Part of the WBCache state machineHandout 6 3In the sequential Spec that we are studying now, a module only makes a transition when anexported routine is invoked. Later, however, we will introduce modules with internal transitions,and then the distinction between the executions and the external behavior will be important.For example, the set of traces generated by the SimpleMemory module includes the followingtrace: (Reset(d)) (Read(a1),d) (Write(a2,d’)) (Read(a2),d’)However, the following trace is not included: (Reset(d)) (Read(a1),d’) (Write(a2,d’)) (Read(a2),d)should have returned d’In general, a trace is included in the external behavior of SimpleMemory if every Read(a)operation returns the last value written to a by a Write, Reset or Swap operation, or returned by aRead operation; if there is no such previous operation, then Read(a) returns an arbitrary value.Implements relationIn order to understand what it means for one state machine to implement another one, it is helpfulto begin by considering what it means for one atomic procedure to implement another. Themeaning of an atomic procedure is a relation between an initial state just before the procedurestarts (sometimes called a ‘pre-state’) and a final state just after the procedure has finished(sometimes called a ‘post-state’). This is often called an ‘input-output relation’. For example, therelation defined by a square-root procedure is that the post-state is the same as the pre-state,except that the square of the procedure result is close enough to the argument.We say that procedure P implements spec S if the relation defined by P (considered as a set ofordered pairs) is a subset of the relation defined by S. This means that P never does anything thatS couldn’t do. However, P doesn’t have to do everything that S can do. An implementation ofsquare root is probably deterministic and always returns the same result for a given argument.Even though the spec allows several results (all the ones that are within the specified tolerance),we don’t require an implementation to be able to produce all of them; instead we are satisfiedwith one.Actually this is not enough. The definition we have given allows P’s relation to be empty, that is,it allows P not to terminate. This is usually called ‘partial correctness’. In addition, we usuallywant to require that P’s relation be total on the domain of S; that is, P must produce some resultwhenever S does. The combination of partial correctness and termination is usually called ‘totalcorrectness’.Now we are ready to consider modules with state. Suppose that T and S are any modules thathave the same external interface (set of procedures that are exported and hence may be invokedexternally). In this discussion, we will often refer to S as the specification module and T as theimplementation . Then we say that T implements S if every trace of T is also a trace of S. That is,the set of traces generated by T is a subset of the set of traces generated by S.Handout 6 4This says that any external behavior of the implementation T must also be an external behavior ofthe spec S. Another way of looking at this is that we shouldn’t be able to tell by looking at theimplementation that we aren’t looking at the spec, so we have to be able to explain everybehavior of T as a possible behavior of S.The reverse, however, is not true. We do not insist that the implementation must exhibit everybehavior allowed by the spec. In the case of the simple memory the spec is completelydeterministic, so the implementations cannot take advantage of this freedom. In general,however, the spec may allow lots of behaviors and the implementation


View Full Document

MIT 6 826 - Study Notes

Documents in this Course
Consensus

Consensus

10 pages

Load more
Download Study Notes
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Study Notes and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Study Notes 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?