Assignments Automated Reasoning

General

Assignment 1

  relation: TYPE = pred[[T, T]]

  R, S: VAR relation

  x, y, z: VAR T

  star(R: relation): relation =
      (LAMBDA (x, y):
         (EXISTS (f: [nat -> T], n: nat):
            f(0) = x AND
             f(n) = y AND
              (FORALL (i: nat): i < n IMPLIES R(f(i), f(i + 1)))))

  star_reflexive: LEMMA reflexive?(star(R))

  star_implied: LEMMA (FORALL (x,y): R(x,y) IMPLIES star(R)(x,y))

  star_preserves_symmetry: LEMMA symmetric?(R) IMPLIES symmetric?(star(R))

  star_transitive: LEMMA transitive?(star(R))

Assignment 2

Assignment 3

• Give a formal specification of the program with one or more Hoare triples.
• Give a program (in a programming language like Modula-3 or C) that satisfies the specification.
• Prove the program with PVS and the "programs" prelude. Take care to prove all TCCs generated (verify this at the end with "prove-importchain").
• Write a report that explains the formal specification, the program, and its proof. Don't dwell on details, but carefully bridge the gap between the description below and the formal specification.
• Give the report (on paper) to Wim Hesselink and send the pvs-dump file to wim@cs.rug.nl.
• It is appreciated when you generalize the problem, provided you carefully indicate how the general version is instantiated to solve the special case.

Assignment 4

• whenever one of the prisoners claims that they have all visited the interrogation room, then this is correct;
• eventually, one of the prisoners will claim. (Hint: use acceptance labels and check for acceptance cycles, see the Introduction to the Model Checker Spin, p. 3, and the Concise Promela Reference.)

Assignment 5

Assignment "Bounded Buffer"

Model this program in Promela to show mutual exclusion and absence of deadlock. Show that products are always stored in empty slots and are always retrieved from full slots. Show that deadlock does not occur. Show that deadlock can occur when the producers, or the consumers can terminate. What choices for the numbers can you accommodate?

Assignment "Readers and Writers"

Model the program in Promela. Allow readers and writers to terminate. Show mutual exclusion and absence of deadlock. What choices for the numbers can you accommodate? Explain the warnings for superfluous code. Do you agree? Can you remove more superfluous code than SPIN observes?

Assignment "Exercise 7.2"

Given are two shared integer variables, x and y, initially 0, and the integer constants a,b > 0 and c,d >= 0. These actions are to be synchronized in such a way that they are executed atomically and preserve the safety conditions x <= y + c and y <= x + d; this should be done as nodeterminately as possible. Reduce the problem to a problem with a finite state space, and write in Promela an algorithm based on split binary semaphores, satisfying the requirements. Show that it does not lead to unnecessary deadlock. Use SPIN to determine the number of reachable states for some choices of the parameters. Can you generalize and prove some facts about this number?

Assignment "Two chambers" (about fairness)

   proctype user(self) {
     do
     :: break /* processes are allowed to leave */
     :: enter chamber[toggle], possibly changing toggle
        wait until toggle has changed
        P(sema)
        CS
        V(sema)
        exit chamber, possibly changing toggle
     od
   }

Assignment Leader Election in a Ring

Model the protocol in Promela and test it with Spin. Set the values of priv.self by means of a function like f(self) = (a*self+b) % 17, for some pairs a, b. Argue that your testing indicates (in)correctness of the protocol. Discuss safety and liveness.

Assignment Barrier synchronization for possibly terminating threads

Given are N environment threads (see below). At certain points in the computation, these threads need to wait for all other threads before they proceed with the next part of the computation. The environment threads can also nondeterministically terminate. Implement this synchronization by N barrier threads, that each communicate with its own environment thread by means of synchronous channels out[p] and in[p], and with each other via channels or shared variables. Accomplish this by implementing "synchronizer" and "logout". These program fragments are not allowed to access the shared variables activeCnt, wCnt, toggle, out, and in.

Test the safety of your solution with the "assert" that is given. Test its liveness also.
Hint: see Sections 2.5, 4.4, etc. of the Collegedictaat on Concurrent Programming (in English), written by Wim Hesselink.

#define Nproc 4
byte activeCnt = Nproc ; 
byte wCnt = 0 ;
bit toggle ;
chan out[Nproc] = [0] of {bit} ;
chan in[Nproc] = [0] of {bit} ;

proctype environ(byte self) {
  bit tog ;
  do
  :: // noncritical activity ;
     atomic {
       assert tog == toggle ;
       tog = ! tog ;
       wCnt ++ ;
       if 
       :: wCnt == activeCnt -> 
          toggle = ! toggle ;
          wCnt = 0 
       :: else
       fi ;
       out[self]!1
     } 
     // AWAIT:
     in[self]?_ 
  :: atomic {   // announce termination:
       activeCnt -- ;
       if 
       :: activeCnt == wCnt ->
          toggle = ! toggle ;
          wCnt = 0 
       :: else
       fi ;
       out[self]!0 ;
       break 
     }
  od 
}

proctype barrier(byte self) {
  do 
  :: out[self]?1 -> 
     "synchronizer" ;
     in[self]!0 
  :: out[self]?0 ->
     "logout" ;
     break
  od 
}