Semaphore Mutual Exclusion

This example was used in "Abstract and Model Check while you Prove" presented by Saidi and Shankar at CAV 99.

Our method proves mutual exclusion automatically.

;;; Semaphore based mutual exclusion
;;;
;;; Original PVS description can be found in "Abstract and Model Check while
;;; you Prove" by Saidi and Shankar in CAV 99.

(let ((idle 0)
      (wait 1)
      (critical 2))

  (murphi-program

   (global-state (pc1 rat)
                 (pc2 rat)
                 (sem rat))

   (initialize (progn
                 (setq pc1 idle)
                 (setq pc2 idle)
                 (setq sem 1)))

   ;; Process 1
   (rules
    (==> (and (= pc1 idle) (> sem 0))
         (progn
           (setq sem (- sem 1))
           (setq pc1 critical)))

    (==> (and (= pc1 idle) (<= sem 0))
         (progn
           (setq sem (- sem 1))
           (setq pc1 wait)))

    (==> (and (= pc1 wait) (> sem 0))
         (setq pc1 critical))

    (==> (and (= pc1 critical) (<= sem 0))
         (progn
           (setq sem (+ sem 1))
           (setq pc1 idle))))

   ;; Process 2
   (rules
    (==> (and (= pc2 idle) (> sem 0))
         (progn
           (setq sem (- sem 1))
           (setq pc2 critical)))

    (==> (and (= pc2 idle) (<= sem 0))
         (progn
           (setq sem (- sem 1))
           (setq pc2 wait)))

    (==> (and (= pc2 wait) (> sem 0))
         (setq pc2 critical))

    (==> (and (= pc2 critical) (<= sem 0))
         (progn
           (setq sem (+ sem 1))
           (setq pc2 idle))))

   (invariant (not (and (= pc1 critical) (= pc2 critical))))

   (abstraction

    ;; Initial predicates
    (B0 (= pc1 critical))
    (B1 (= pc2 critical))

    ;; Iteration 1
    (C01 (< (+ 1 (* -1 SEM)) 0))

    ;; Iteration 2
    (C02 (= (+ 1 (* -1 SEM)) 0))

    ;; Iteration 3
    (C03 (< (+ 0 (* -1 SEM)) 0))

    ;; Iteration 4
    (C04 (= PC2 1))

    ;; Iteration 5
    (C05 (= PC1 1))

    ;; Iteration 6
    (C06 (< (+ -1 (* -1 SEM)) 0)))))