abs_tm_nontr: THEORY

 % Proving trivial transactional memory implementation with non-transactional
 % memory accesses (the TM knows about the non-transactional)

 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]

  % == Implementation specifics:
  % the conflcit - for this implementation  both conflict and memory consistency
  is_conflict(commit_trans, other_trans: Q): bool  =
     (EXISTS (i,j: posnat):
        i <= other_trans`size             AND 
        j <= commit_trans`size            AND 
        other_trans`entry(i)`act  = READ  AND
        commit_trans`entry(j)`act = WRITE AND
        commit_trans`entry(j)`adr = other_trans`entry(i)`adr)

  % hard to explain...
  same_queues_same_conflicts: LEMMA
    FORALL (proj1,proj2: [ID -> Q], id1: ID):
      FORALL (id2: ID):
        (eql(proj1(id1),proj2(id1)) AND
         eql(proj1(id2),proj2(id2)))   IMPLIES
           (is_conflict(proj1(id1),proj1(id2)) IFF
            is_conflict(proj2(id1),proj2(id2))) 

  % new_mem is memory of the primed state if 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 - Non-transactional Read:
          (EXISTS (id: ID, adr: ADDRESS): 
             empty(st_c`trans(id)) 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 := NT_READ, adr := adr, val := read_val#),
                                doomed := doom_others(is_conflict, id, st_c`trans 
                                            WITH [id := add_ntread(id,adr,read_val,null1)] , st_c`doomed)])
       % t2 - Non-transactional Write:
       OR (EXISTS (id: ID, adr: ADDRESS, val: VALUE): 
             empty(st_c`trans(id)) AND
             stp_c = st_c WITH [out   := (#id := id, act := NT_WRITE, adr := adr, val := val#),
                                mem    := update_mem(st_c`mem, add_write(id,adr,val,null1), id),
                                doomed := doom_others(is_conflict, id, st_c`trans WITH [id := add_ntwrite(id,adr,val,null1)] , st_c`doomed)])
       % t3 - Open:
       OR (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))]])
       % t4 - 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
             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
             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
             st_c`doomed(id) = FALSE                                  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],
                                doomed := doom_others(is_conflict, id, st_c`trans, st_c`doomed)])
       % t7 - abort
       OR (EXISTS (id: ID):  
             NOT empty(st_c`trans(id))                                             AND
             NOT read_events_consistent_with_mem(st_c`trans(id),st_c`mem) AND 
             stp_c = st_c WITH [out    := (#id := id, act := ABORT, adr := 0, val := 0#),
                                trans  := st_c`trans  WITH [(id) := null1],
                                doomed := st_c`doomed WITH [(id) := FALSE]])
       % 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 #)            


  % ==== 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 - Non-transactional Read
           (EXISTS (id: ID):  
             (EXISTS (adr: nat):
                (EXISTS (val: nat):
                  NOT is_active(st_a`q,id) AND
                  NOT st_a`doomed(id)      AND
                  stp_a = st_a WITH [out := (#id := id, act := NT_READ, adr := adr, val := val#),
                                     doomed := doom_others(is_conflict,id,project(add_ntread(id,adr,val,st_a`q)),st_a`doomed)])))
       % a2 - Non-transactional Write
       OR  (EXISTS (id: ID):  
             (EXISTS (adr: nat):
                (EXISTS (val: nat):
                  NOT is_active(st_a`q,id) AND
                  NOT st_a`doomed(id)      AND
                  stp_a = st_a WITH [out    := (#id := id, act := NT_WRITE, adr := adr, val := val#),
                                     mem    := update_mem(st_a`mem, st_a`q, id),
                                     q      := fix_q_after_commit(is_conflict,id,add_ntwrite(id,adr,val,st_a`q)),
                                     doomed := doom_others(is_conflict,id,project(add_ntwrite(id,adr,val,st_a`q)),st_a`doomed)])))
       % a3 - Open:
       OR  (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)
       % a4 - 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#)]))))
       % a5 - 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#)]))))
       % a8 - 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]])) 
       % a6,a7,a9 and a10 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, st_a`q, 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#) 

  % ==== 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):
      empty(st_c`trans(id)) IMPLIES NOT st_c`doomed(id))

  % 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): (NOT st_c`doomed(id)) IMPLIES %st_a`doomed(id)
                            eql(st_c`trans(id),project(st_a`q)(id)))             AND
       (FORALL (id: ID): (empty(st_c`trans(id))) IMPLIES 
                            empty(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 abs_tm_nontr