Properties of the Tatami Protocol

We want to prove

coherence(PROTOCOL) .
Attribute coherence requires us to prove the following subgoals:
  • S2,S1:State E:Elt (((database(S1) = database(S2)) and (temp-mem(S1) = temp-mem(S2))) and (U:User (not-ack(U,S1) = not-ack(U,S2)))    implies
           (database(submit(E,S1)) = database(submit(E,S2))     and
           temp-mem(submit(E,S1)) = temp-mem(submit(E,S2))     and
           U:User (not-ack(U,submit(E,S1)) = not-ack(U,submit(E,S2))) ))
    .
    • Quantifier elimination introduces new constants e :Elt and s2 s1 :State .
    • Implication elimination assumes    database(s1) = database(s2)     and
         temp-mem(s1) = temp-mem(s2)     and
         U:User (not-ack(U,s1) = not-ack(U,s2))
      .
    • Change hypothesis    database(s1) = database(s2)     and
         temp-mem(s1) = temp-mem(s2)     and
         U:User (not-ack(U,s1) = not-ack(U,s2))
      to rewritng rule.
    • Conjunction elimination introduces subgoals as follows:
      1. database(submit(e,s1)) = database(submit(e,s2)) .
        • Show database(submit(e,s1)) = database(submit(e,s2)) by reduction.
      2. temp-mem(submit(e,s1)) = temp-mem(submit(e,s2)) .
        • Show temp-mem(submit(e,s1)) = temp-mem(submit(e,s2)) by reduction.
      3. forall U:User (not-ack(U,submit(e,s1)) = not-ack(U,submit(e,s2))) .
  • S2,S1:State E:Elt (((database(S1) = database(S2)) and (temp-mem(S1) = temp-mem(S2))) and (U:User (not-ack(U,S1) = not-ack(U,S2)))    implies
           (database(insert(E,S1)) = database(insert(E,S2))     and
           temp-mem(insert(E,S1)) = temp-mem(insert(E,S2))     and
           U:User (not-ack(U,insert(E,S1)) = not-ack(U,insert(E,S2))) ))
    .
    • Quantifier elimination introduces new constants e :Elt and s2 s1 :State .
    • Implication elimination assumes    database(s1) = database(s2)     and
         temp-mem(s1) = temp-mem(s2)     and
         U:User (not-ack(U,s1) = not-ack(U,s2))
      .
    • Change hypothesis    database(s1) = database(s2)     and
         temp-mem(s1) = temp-mem(s2)     and
         U:User (not-ack(U,s1) = not-ack(U,s2))
      to rewritng rule.
    • Conjunction elimination introduces subgoals as follows:
      1. database(insert(e,s1)) = database(insert(e,s2)) .
        • Show database(insert(e,s1)) = database(insert(e,s2)) by reduction.
      2. temp-mem(insert(e,s1)) = temp-mem(insert(e,s2)) .
        • Show temp-mem(insert(e,s1)) = temp-mem(insert(e,s2)) by reduction.
      3. forall U:User (not-ack(U,insert(e,s1)) = not-ack(U,insert(e,s2))) .
  • S2,S1:State E:Elt (((database(S1) = database(S2)) and (temp-mem(S1) = temp-mem(S2))) and (U:User (not-ack(U,S1) = not-ack(U,S2)))    implies
           (database(receive(E,S1)) = database(receive(E,S2))     and
           temp-mem(receive(E,S1)) = temp-mem(receive(E,S2))     and
           U:User (not-ack(U,receive(E,S1)) = not-ack(U,receive(E,S2))) ))
    .
    • Quantifier elimination introduces new constants e :Elt and s2 s1 :State .
    • Implication elimination assumes    database(s1) = database(s2)     and
         temp-mem(s1) = temp-mem(s2)     and
         U:User (not-ack(U,s1) = not-ack(U,s2))
      .
    • Change hypothesis    database(s1) = database(s2)     and
         temp-mem(s1) = temp-mem(s2)     and
         U:User (not-ack(U,s1) = not-ack(U,s2))
      to rewritng rule.
    • Conjunction elimination introduces subgoals as follows:
      1. database(receive(e,s1)) = database(receive(e,s2)) .
        • Show database(receive(e,s1)) = database(receive(e,s2)) by reduction.
      2. temp-mem(receive(e,s1)) = temp-mem(receive(e,s2)) .
        • Show temp-mem(receive(e,s1)) = temp-mem(receive(e,s2)) by reduction.
      3. forall U:User (not-ack(U,receive(e,s1)) = not-ack(U,receive(e,s2))) .
  • S2,S1:State U':User E:Elt (((database(S1) = database(S2)) and (temp-mem(S1) = temp-mem(S2))) and (U:User (not-ack(U,S1) = not-ack(U,S2)))    implies
           (database(ack(U',E,S1)) = database(ack(U',E,S2))     and
           temp-mem(ack(U',E,S1)) = temp-mem(ack(U',E,S2))     and
           U:User (not-ack(U,ack(U',E,S1)) = not-ack(U,ack(U',E,S2))) ))
    .
    • Quantifier elimination introduces new constants e :Elt and u' :User and s2 s1 :State .
    • Implication elimination assumes    database(s1) = database(s2)     and
         temp-mem(s1) = temp-mem(s2)     and
         U:User (not-ack(U,s1) = not-ack(U,s2))
      .
    • Change hypothesis    database(s1) = database(s2)     and
         temp-mem(s1) = temp-mem(s2)     and
         U:User (not-ack(U,s1) = not-ack(U,s2))
      to rewritng rule.
    • Conjunction elimination introduces subgoals as follows:
      1.    database(ack(u',e,s1)) = database(ack(u',e,s2))     and
           temp-mem(ack(u',e,s1)) = temp-mem(ack(u',e,s2))
        • Conjunction elimination introduces subgoals as follows:
          1. database(ack(u',e,s1)) = database(ack(u',e,s2))
            • Show database(ack(u',e,s1)) = database(ack(u',e,s2)) by reduction.
          2. temp-mem(ack(u',e,s1)) = temp-mem(ack(u',e,s2))
            • Show temp-mem(ack(u',e,s1)) = temp-mem(ack(u',e,s2)) by reduction.
      2. U:User (not-ack(U,ack(u',e,s1)) = not-ack(U,ack(u',e,s2)))


This page was generated
by Kumo on Fri Jun 12 12:32:43 PDT 1998 from code written by Grigore Rosu,