ltm: THEORY

 % Eager conflict detection and lazy memory management (LTM);
 % Conflict: eager invalidation & no two writes to the same location;
 % Arbitration: aborting the one that requests the second conflicting access;

 BEGIN

  ID: TYPE = nat
  ID1: ID =  0
 
  IMPORTING tm[ID,ID1] % procedures and lemmas for transactional memories

  % The observables
  OBSERVATION_DOMAIN: TYPE = [#out: EVENT#]

  % The concrete system
  FAIRNESS_DOMAIN_C:  TYPE 
  STATE_C:            TYPE = [#out: EVENT, mem: MEM, trans: TRANS, doomed: DOOM#]
 
  % The abstract system
  FAIRNESS_DOMAIN_A:  TYPE
  STATE_A:            TYPE = [#out: EVENT, mem: MEM, q: Q, doomed: DOOM#]

  % Importing the full system
  IMPORTING SYSTEM[STATE_C, FAIRNESS_DOMAIN_C, STATE_A, FAIRNESS_DOMAIN_A, OBSERVATION_DOMAIN]
  BI_PREDICATE_C: TYPE = BI_PREDICATE[STATE_C, OBSERVATION_DOMAIN, FAIRNESS_DOMAIN_C]
  BI_PREDICATE_A: TYPE = BI_PREDICATE[STATE_A, OBSERVATION_DOMAIN, FAIRNESS_DOMAIN_A]

  % == TM specifics:
  % The conflict - for this implementation  both conflict and memory consistency
  is_conflict(accessing_trans, other_trans: Q): bool  =
     (EXISTS (i,j: posnat):
        i <= other_trans`size                                   AND 
        j <= accessing_trans`size                               AND 
        accessing_trans`entry(j)`id /= other_trans`entry(i)`id  AND
        accessing_trans`entry(j)`adr = other_trans`entry(i)`adr AND
        ((accessing_trans`entry(j)`act = WRITE AND
          (other_trans`entry(i)`act  = READ OR  
           other_trans`entry(i)`act  = WRITE))    OR
         (accessing_trans`entry(j)`act = READ AND
          other_trans`entry(i)`act  = WRITE)))

  % The conflict of this TM is symetric
  conflict_is_symetric: LEMMA
    FORALL (trans1,trans2: Q):
      is_conflict(trans1,trans2) IMPLIES
        is_conflict(trans2,trans1)

  % Conflict occurs if the accessing client is reading
  % and a pending transaction of a different client consists 
  % of a write to the same address
  conflicting_new_read_event: AXIOM
    FORALL (accessing_trans, other_trans: Q): 
      (FORALL (e: EVENT, old_accessing_trans: Q):
         (eql(accessing_trans,add(e,old_accessing_trans)) AND
          NOT is_conflict(old_accessing_trans,other_trans)) IMPLIES
            (EXISTS (i: posnat):
               i <= other_trans`size            AND   
               e`id /= other_trans`entry(i)`id  AND
               e`adr = other_trans`entry(i)`adr AND
               e`act = READ                     AND
               other_trans`entry(i)`act = WRITE))

  % Conflict occurs if the accessing client is writing
  % and a pending transaction of a different client consists 
  % of a read or a write to the same address
  conflicting_new_write_event: AXIOM
    FORALL (accessing_trans, other_trans: Q): 
      (FORALL (e: EVENT, old_accessing_trans: Q):
         (eql(accessing_trans,add(e,old_accessing_trans)) AND
          NOT is_conflict(old_accessing_trans,other_trans)) IMPLIES
            (EXISTS (i: posnat):
               i <= other_trans`size              AND   
               e`id /= other_trans`entry(i)`id    AND
               e`adr = other_trans`entry(i)`adr   AND
               e`act = WRITE                      AND
               (other_trans`entry(i)`act = READ OR
                other_trans`entry(i)`act = WRITE)))

  % If there are no conflict between projectings over two clients, then
  % there aren't any after removing events from the quueue:

  % If there was no conflict before committing then there is none
  % after, since events are only removed from the q
  not_conf_imp_not_conf_after_commit: AXIOM
    (FORALL (q: Q)(id1,id2: ID):
       NOT is_conflict(project(q)(id1),project(q)(id2)) IMPLIES
         (FORALL (commit_id: ID):
            NOT is_conflict(project(fix_q_after_commit(is_conflict, commit_id, q))
                                   (id1),
                            project(fix_q_after_commit(is_conflict, commit_id, q))
                                   (id2))))

  % If there was no conflict before aborting then there is none
  % after, since events are only removed from the q
  not_conf_imp_not_conf_after_abort: AXIOM
    (FORALL (q: Q)(id1,id2: ID):
       NOT is_conflict(project(q)(id1),project(q)(id2)) IMPLIES
         (FORALL (commit_id: ID):
            NOT is_conflict(project(projection(not_of_id(commit_id), q))
                                   (id1),
                            project(projection(not_of_id(commit_id), q))
                                   (id2))))

  % new_mem is memory of the primed state of the imp.
  % mem is the unprimed mem of the spec
  % if the updated mem of spec equals the new mem of imp,
  % and there were no conflicts between read_id and the commit_id
  % then the read events of read_id are still consistent
  not_conflicting_update_mem_preserve_const: AXIOM
    FORALL (q: Q, read_id, commit_id: ID, mem, new_mem: MEM):
      (new_mem = update_mem(mem, project(q)(commit_id),commit_id) AND
       NOT is_conflict(project(q)(commit_id),project(q)(read_id)))   IMPLIES
         read_events_consistent_with_mem(project(q)(read_id), new_mem)

  % == Setting the elements of the concrete system
  st_c, stp_c: VAR STATE_C
 
   % the transition relation
  rho_c: BI_PREDICATE_C = 
    (LAMBDA (st_c, stp_c):
       % t1 - Open:
          (EXISTS (id: ID): 
             empty(st_c`trans(id)) AND
             stp_c = st_c WITH [out   := (#id := id, act := OPEN, adr := 0, val := 0#),
                                trans := st_c`trans WITH [(id) := add_open(id,st_c`trans(id))]])
       % t2 - Read:
       OR (EXISTS (id: ID, adr: ADDRESS): 
             NOT empty(st_c`trans(id))                                               AND 
             NOT some(is_write_of_id(id),st_c`trans(id))                             AND
             NOT (EXISTS (id_other: ID):
                    id_other /= id AND
                    exist(is_write_of_id_to_adr(id_other, adr),st_c`trans(id_other))) AND
             LET read_val = get_read_val(adr,st_c`mem,st_c`trans(id)) IN
             stp_c = st_c WITH [out   := (#id := id, act := READ, adr := adr, val := read_val#),
                                trans := st_c`trans 
                                           WITH [(id) := add_read(id,adr,read_val,st_c`trans(id))]])
       % t5 - Write:
       OR (EXISTS (id: ID, adr: ADDRESS, val: VALUE): 
             NOT empty(st_c`trans(id))                                                 AND
             NOT (EXISTS (id_other: ID):
                    id_other /= id AND
                    exist(is_write_of_id_to_adr(id_other, adr),st_c`trans(id_other)))  AND
             NOT (EXISTS (id_other: ID):
                    id_other /= id AND
                    exist(is_read_of_id_from_adr(id_other, adr),st_c`trans(id_other))) AND
             stp_c = st_c WITH [out   := (#id := id, act := WRITE, adr := adr, val := val#),
                                trans := st_c`trans
                                           WITH [(id) := add_write(id,adr,val,st_c`trans(id))]])
       % t6 - Commit:
       OR (EXISTS (id: ID):  
             NOT empty(st_c`trans(id))                                AND
             read_events_consistent_with_mem(st_c`trans(id),st_c`mem) AND
             stp_c = st_c WITH [out    := (#id := id, act := COMMIT, adr := 0, val := 0#),
                                mem    := update_mem(st_c`mem, st_c`trans(id), id),
                                trans  := st_c`trans  WITH [(id) := null1]])
       % t7 - abort
       OR (EXISTS (id: ID):  
             NOT empty(st_c`trans(id))                                             AND
             stp_c = st_c WITH [out    := (#id := id, act := ABORT, adr := 0, val := 0#),
                                trans  := st_c`trans  WITH [(id) := null1]])
       % Idle:
       OR stp_c = st_c WITH [out := (#id := 0, act := NULL, adr := 0, val := 0#)])

  % observing the concrete system
  obs_c: OBSERVABLE_C = 
    (LAMBDA st_c: 
      (#out := st_c`out#))

  % the full concrete system
  con: CON =
         (# initial := {st_c | st_c`out    = null_event  AND 
                               st_c`mem    = empty_mem   AND 
                               st_c`trans  = init_trans AND 
                               st_c`doomed = init_doomed},
            rho     := rho_c,
            obs     := obs_c,
            justice := empty_justice #)            


  % ==== Setting the elements of the abstract system: ====
  st_a, stp_a: VAR STATE_A

  rho_a: BI_PREDICATE_A = 
    (LAMBDA (st_a, stp_a):
       % a1 - Open:
          (EXISTS (id: ID):  
             NOT is_active(st_a`q,id) AND
             IF st_a`doomed(id) 
               THEN stp_a = st_a WITH [out := (#id := id, act := OPEN, adr := 0, val := 0#)]
               ELSE stp_a = st_a WITH [out := (#id := id, act := OPEN, adr := 0, val := 0#),
                                       q   := add_open(id,st_a`q)]
             ENDIF)
       % a2/a3 - Read:
       OR (EXISTS (id: ID):  
             (EXISTS (adr: nat):
                (EXISTS (val: nat):
                   NOT some(is_write_of_id(id),st_a`q) AND  % simplifying assumption
                   (is_active(st_a`q,id) AND
                    stp_a = st_a WITH [out := (#id := id, act := READ, adr := adr, val := val#),
                                       q   := add_read(id,adr,val,st_a`q)]) OR
                   (st_a`doomed(id) AND
                    stp_a = st_a WITH [out := (#id := id, act := READ, adr := adr, val := val#)]))))
       % a4/a5 - Write:
       OR (EXISTS (id: ID):  
             (EXISTS (adr: nat):
                (EXISTS (val: nat):
                  (is_active(st_a`q,id) AND
                   stp_a = st_a WITH [out := (#id := id, act := WRITE, adr := adr, val := val#),
                                      q   := add_write(id,adr,val,st_a`q)]) OR
                  (st_a`doomed(id) AND
                   stp_a = st_a WITH [out := (#id := id, act := WRITE, adr := adr, val := val#)]))))
       % a6 - Abort:
       OR (EXISTS (id: ID):  
             ((is_active(st_a`q,id) OR st_a`doomed(id)) AND
              stp_a = st_a WITH [out    := (#id := id, act := ABORT, adr := 0, val := 0#),
                                 q      := projection(not_of_id(id),st_a`q),
                                 doomed := st_a`doomed WITH [(id) := FALSE]])) 
       % a7,a8,a9,a10 and a11 were combined into one action - Commit:
       OR (EXISTS (id: ID):  
             (is_active(st_a`q,id)                                          AND
              read_events_consistent_with_mem(project(st_a`q)(id),st_a`mem) AND
              stp_a = st_a WITH [out    := (#id := id, act := COMMIT, adr := 0, val := 0#),
                                 mem    := update_mem(st_a`mem, project(st_a`q)(id), id),
                                 q      := fix_q_after_commit(is_conflict,id,st_a`q),
                                 doomed := doom_others(is_conflict,id,project(st_a`q),st_a`doomed)]))
       % Idle:
       OR stp_a = st_a WITH [out := (#id := 0, act := NULL, adr := 0, val := 0#)])

  % observing the abstract system
  obs_a: OBSERVABLE_A = 
    (LAMBDA st_a: 
      (#out := st_a`out#))

  % the full abstract system
  abs: ABS =
         (# initial :=  {st_a | st_a`out    = null_event AND 
                                st_a`mem    = empty_mem  AND 
                                st_a`q      = null1      AND 
                                st_a`doomed = init_doomed},
            rho     := rho_a, 
            obs     := obs_a,
            justice := empty_justice #) 

  % ==== Checking that con refines abs: ====
  % procedures supporting the invariant of concrete system:

  % the invariant of the system
  inv(st_a,st_c) : bool =
    (FORALL (id :ID):
      read_events_consistent_with_mem(project(st_a`q)(id), st_a`mem)) AND
    (FORALL (id :ID):
      NOT st_c`doomed(id))                                            AND
    (FORALL (id1,id2 :ID):
      NOT is_conflict(project(st_a`q)(id1),project(st_a`q)(id2)))

  % relation between abs and con
  rel: RELATION = 
    (LAMBDA st_c, st_a:
       st_c`out = st_a`out                                                       AND
       st_c`mem = st_a`mem                                                       AND
       st_c`doomed = st_a`doomed                                                 AND
       (FORALL (id: ID): 
          eql(st_c`trans(id),project(st_a`q)(id)))                               AND
       inv(st_a,st_c))

  % a function for constructing a new abstract state (for instantiations)
  st_a(out_i: EVENT, mem_i: ARRAY[nat -> nat], q_i: Q, doomed_i: ARRAY[ID -> bool]): STATE_A = 
    (#out := out_i, mem := mem_i, q := q_i, doomed := doomed_i#)

  % The main lemma: con") refines abs
  abstraction: LEMMA abstract(con,abs)

 END ltm