Exercises

• 13.1 Simplify the verification model developed in section 13.5 such that it is a model of the Java program ReadWriteSafe (Program 7.7). Show that this model does not violate the property SAFE_RW and that it violates the WRITE progress property.

• 13.2 Develop a verification model for the Semaphore class (Program 5.3) and use it in verifying that the SEMADEMO program of Chapter 5 preserves the mutual exclusion property (section 7.1.2):

   property MUTEX = (p[i:1..3].enter->p[i].exit->MUTEX).

• In addition, generate an error trace for the situation in which the semaphore is initialized to 2.

• 13.3 The following FSP specifies the safety property for barrier synchronization. Each process must execute its before action before all processes execute the common sync action.

   Pspec = (before -> sync -> Pspec). property    ||SAFEBARRIER = (p[1..3]:Pspec)                    /{sync/p[1..3].sync}\{sync}.

• Verify that the monitor Barrier with a sync method that implements barrier synchronization (as required in the solution to Exercise 5.5) satisfies the above property.

• 13.4 Verify that the SimpleAllocator monitor of Program 9.1 satisfies the property ALLOCATOR in the system CHECK, both shown below:

   property   ALLOCATOR(M=3) = BALL[M],   BALL[b:0..M]   = (when (b>0) get[i:1..b] -> BALL[b-i]                    |put[j:1..M]      -> BALL[b+j]                    ). PLAYER(I=1) = (get.call -> GET(I);PLAYING), PLAYING     = (put.call -> PUT(I);PLAYER). ||CHECK = (player[1..3]:PLAYER(1)           ||player[4..Nthread]:PLAYER(3)           ||SimpleAllocator(N)           ||player[1..N]::ALLOCATOR(N)           ).

• In addition, determine which of the following progress properties are satisfied by the system CHECKLIVE shown below:

   progress EXPERT = {player[1..3].get[1..N]} progress NOVICE = {player[4..N].get[1..N]} ||CHECKLIVE = CHECK >> {player[1..N].put.call}.