CSCI P415/P515 HOMEWORK

CSCI P415/515

Fri Jan 6 15:18:04 EST 2012 [SDJ]

Homework Assignment

Introduction to SMV

Instructions:

Run vw on or.smv [SMV] and verify the SPEC formulas using the verify-all command in the Prop menu, or its keyboard shortcut, "a"
For those SPEC statements that are false, examine the counter-scenerios to determine the cause of the failure.
Add SPEC formulas saying:
1. "It is (im)possible for the first event to be missed."
2. "It is (im)possible for the first event to counted twice."
3. "It is (im)possible to count one event three times."
Construct these formulas to make SMV show you how the eventualities are (im)possible.
Submit a report, report.pdf explaining your findings.

Notes and Hints

Lecture Notes on modeling the Observer-Reporter system in SMV [PDF]
SMV model or.smv. Add SPEC statements to show that events can be missed or counted more than once.
Formulate these conditions in the negative in order to generate counter-scenarios. For example, if you want to prove, "It is possible for an event to be counted twice," code a SPEC that says, "It is impossible for an event to be counted twice." That way, if it is in fact possible, SMV will show you one way it can happen.

The Observer-Reporter Problem

An observer process is monitoring asynchronous events. When it senses an event it increments a counter variable. In pseudocode:

    Observer: while true do
                begin
                await EVENT;
                COUNT := COUNT + 1;
                end;

A reporter process periodically prints the event tally and clears the counter.

    Reporter: while true do
                begin
                wait INTERVAL seconds;
                print(TIME, COUNT);
                COUNT := 0;
                end;

These higher level instructions must be compiled into a "machine-level" model whose atomic instructions can only:

MOV source, destination copies a word of data one location to another, but does not alter that data. The source and target locations may be processor registers or memory addresses.
OP opnd1, opnd2, result performs an arithmetic-logical operation OP on operands opnd1 and opnd2 leaving the result in location result. Locations opnd1, opnd2 and result must all be processor registers.
JMP label transfers control to another point in the program.

The machine model, then, is a traditional one in which "memory" can only hold data, and in order to manipulate date, it must first be brought into the registers of the processor. At this level of atomicity, the processes are:

OBSERVER: {wait for EVENT to occur}
          MOV count, r1   -- retrieve the value of COUNT
          ADD 1, r1, r1   -- increment it
          MOV r1, count   -- store the result
          JMP OBSERVER

REPORTER: {wait for an INTERVAL of time}
          MOV count, r1   -- retrieve the value of COUNT
          MOV 0, count    -- clear the global value
          {Print r1}      -- log the value
          JMP REPORTER