Skip to content

Verification Primer

Jump to bottom Edit New page
tomahawkins edited this page Apr 12, 2011 · 7 revisions

Arbiter Verification

In this example we will design and verify a simple arbiter. As inputs, the arbiter will requests from three devices competing for a shared resource, and the arbiter will output three booleans signals telling each device whether they have been granted the resource (Arbiter.hs):

-- Input requests.
requestA = input bool ["requestA"]
requestB = input bool ["requestB"]
requestC = input bool ["requestC"]

-- Output variables.
grantA = global bool ["grantA"] False
grantB = global bool ["grantB"] False
grantC = global bool ["grantC"] False

-- Some helpers to reference of the output variables expressions.
grantA' = ref grantA
grantB' = ref grantB
grantC' = ref grantC

Some properties we would like the arbiter to adhere to include:

  • At most, only one request is granted at a time.
  • If a grant is issued, corresponding device must be making a request.
  • If any request is raised, a grant must be made.

Based on these requirements we can formulate an ImProve specification:

arbiterSpecification :: Stmt ()
arbiterSpecification = do
  -- Only one request is granted at a time.
  theorem "at most one grant" 1 [] $ not_ grantA' &&. not_ grantB' &&. not_ grantC'
                                 ||.      grantA' &&. not_ grantB' &&. not_ grantC'
                                 ||. not_ grantA' &&.      grantB' &&. not_ grantC'
                                 ||. not_ grantA' &&. not_ grantB' &&.      grantC'

  -- A grant must correspond to a request.
  theorem "grant implies request A" 1 [] $ grantA' --> requestA
  theorem "grant implies request B" 1 [] $ grantB' --> requestB
  theorem "grant implies request C" 1 [] $ grantC' --> requestC

  -- Any request implies a grant.
  theorem "any request implies a grant" 1 [] $ requestA ||. requestB ||. requestC
                                           --> grantA'  ||. grantB'  ||. grantC'
  return ()

Note the implication boolean operator (a --> b), which is equivalent to (not_ a ||. b).

With a formal specification in place, we can now construct an implementation:

arbiter :: Stmt ()
arbiter = do
  case_ $ do
    requestA ==> do
      grantA <== true
      grantB <== false
      grantC <== false
    requestB ==> do
      grantA <== true
      grantB <== false
      grantC <== true
    requestC ==> do
      grantA <== false
      grantB <== false
      grantC <== true

To conduct the formal verification, add 'verify' to Arbiter.hs:

main :: IO ()
main = verify "yices" $ arbiter >> arbiterSpecification  -- This binds the arbiter to the specification.

Running the verification with:

$ runhaskell Arbiter.hs

yields:

at most one grant              FAILED: disproved basis (see at most one grant.trace)
grant implies request A        FAILED: disproved basis (see grant implies request A.trace)
grant implies request B        proved
grant implies request C        FAILED: disproved basis (see grant implies request C.trace)
any request implies a grant    proved

Three properties have failed, meaning ImProve was able to find three concrete cases where the implementation failed the specification. For each case, ImProve produces a counter examples that show each precise failure. Let's take a close look at 'at most one grant.trace':

(step 0)
(state)                      : grantA   == false
(state)                      : grantB   == false
(state)                      : grantC   == false
(input)                      : requestA <== false
(input)                      : requestB <== true
(input)                      : requestC <== false
                             : ifelse false:
                             :     ifelse true:
                             :         grantA <== true
                             :         grantB <== false
                             :         grantC <== true
at most one grant            : theorem assertion FAILED

This counter example shows that at initialization the three grant variables are set to false, and that of the three inputs, only device B is issuing a request. But the outcome is that grantA and grantC are set to true and grantB is set to false; clearly not desired behavior. We can easily trace this bug back to the implementation:

arbiter :: Stmt ()
arbiter = do
  case_ $ do
    requestA ==> do
      grantA <== true
      grantB <== false
      grantC <== false
    requestB ==> do
      grantA <== true    -- Bug!!!
      grantB <== false   -- Bug!!!
      grantC <== true    -- Bug!!!
    requestC ==> do
      grantA <== false
      grantB <== false
      grantC <== true

We fix the bugs:

arbiter :: Stmt ()
arbiter = do
  case_ $ do
    requestA ==> do
      grantA <== true
      grantB <== false
      grantC <== false
    requestB ==> do
      grantA <== false  --
      grantB <== true   -- That's better.
      grantC <== false  --
    requestC ==> do
      grantA <== false
      grantB <== false
      grantC <== true

Rerunning the verification now yields:

at most one grant              proved
grant implies request A        inconclusive: unable to proved step (see grant implies request A.trace)
grant implies request B        inconclusive: unable to proved step (see grant implies request B.trace)
grant implies request C        inconclusive: unable to proved step (see grant implies request C.trace)
any request implies a grant    proved

This time, thought nothing fails, we have a bunch of inconclusive results. The first thing to try is increasing the search depth from k = 1 to k = 2:

  theorem "grant implies request A" 2 [] $ grantA' --> requestA

With k = 2, this produces a concrete failure:

at most one grant              proved
grant implies request A        FAILED: disproved basis (see grant implies request A.trace)
grant implies request B        inconclusive: unable to proved step (see grant implies request B.trace)
grant implies request C        inconclusive: unable to proved step (see grant implies request C.trace)
any request implies a grant    proved

The counter example 'grant implies request A.trace' shows:

(step 0)
(state)                      : grantA   == false
(state)                      : grantB   == false
(state)                      : grantC   == false
(input)                      : requestA <== true
(input)                      : requestB <== false
(input)                      : requestC <== false
                             : ifelse true:
                             :     grantA <== true
                             :     grantB <== false
                             :     grantC <== false
grant implies request A      : theorem assertion passed
(step 1)
(state)                      : grantA   == true
(state)                      : grantB   == false
(state)                      : grantC   == false
(input)                      : requestA <== false
(input)                      : requestB <== false
(input)                      : requestC <== false
                             : ifelse false:
                             :     ifelse false:
                             :         ifelse false:
grant implies request A      : theorem assertion FAILED

This counter example shows that in step 0, device A issues a request, which is granted. But then in step 1, device A drops it's request, but grantA fails to drop low. Upon inspection of the implementation, we find we forgot to handle the case when no requests are made -- an easy bug to fix:

arbiter :: Stmt ()
arbiter = do
  case_ $ do
    requestA ==> do
      grantA <== true
      grantB <== false
      grantC <== false
    requestB ==> do
      grantA <== false
      grantB <== true
      grantC <== false
    requestC ==> do
      grantA <== false
      grantB <== false
      grantC <== true
    true ==> do         -- Forgot to clear all the grants when no requests are made.
      grantA <== false
      grantB <== false
      grantC <== false

Now rerunning the verification produces clean results:

at most one grant              proved
grant implies request A        proved
grant implies request B        proved
grant implies request C        proved
any request implies a grant    proved

Our final Aribter.hs file looks like this:

module Main where

import Language.ImProve

main = verify "yices" $ arbiter >> arbiterSpecification

requestA = input bool ["requestA"]
requestB = input bool ["requestB"]
requestC = input bool ["requestC"]

grantA = global bool ["grantA"] False
grantB = global bool ["grantB"] False
grantC = global bool ["grantC"] False
grantA' = ref grantA
grantB' = ref grantB
grantC' = ref grantC

arbiterSpecification :: Stmt ()
arbiterSpecification = do
  -- Only one request is granted at a time.
  theorem "at most one grant" 1 [] $ not_ grantA' &&. not_ grantB' &&. not_ grantC'
                                 ||.      grantA' &&. not_ grantB' &&. not_ grantC'
                                 ||. not_ grantA' &&.      grantB' &&. not_ grantC'
                                 ||. not_ grantA' &&. not_ grantB' &&.      grantC'

  -- A grant must correspond to a request.
  theorem "grant implies request A" 1 [] $ grantA' --> requestA
  theorem "grant implies request B" 1 [] $ grantB' --> requestB
  theorem "grant implies request C" 1 [] $ grantC' --> requestC

  -- Any request implies a grant.
  theorem "any request implies a grant" 1 [] $ requestA ||. requestB ||. requestC
                                           --> grantA'  ||. grantB'  ||. grantC'

  return ()

arbiter :: Stmt ()
arbiter = do
  case_ $ do
    requestA ==> do
      grantA <== true
      grantB <== false
      grantC <== false
    requestB ==> do
      grantA <== false
      grantB <== true
      grantC <== false
    requestC ==> do
      grantA <== false
      grantB <== false
      grantC <== true
    true ==> do
      grantA <== false
      grantB <== false
      grantC <== false
Add a custom footer
Add a custom sidebar
Clone this wiki locally