<commit_before>open ../archs/exec_arm8L[E]
open ../models/aarch64_txn[E] as M

module arm8_lock_elision[E]

pred apply_map[X,X':Exec_Arm8L, map:E->E] { 

  map in (X.EV one-> X'.EV)

  // no critical sections remain
  no X'.(LkT + UkT + LkN + UkN)

  // suppose we don't have transactions in the source program
  no X.stxn

  // events in the same critical section (where the critical
  // section is one that is to be transactionalised), map to events 
  // in the same transaction.
  (X.EV - X.UkT) <: scst[X] :> (X.EV - X.UkT) = map.(X'.stxn).~map

  // the set of lock-related events introduced by the mapping
  let L = map[X.(LkT + UkT + LkN + UkN)] {

    // Mildly interesting observation: transactional memory models
    // are not monotonic w.r.t. adding sequencing edges

    X'.sthd = ~map.(X.sthd).map

    all e1, e2 : X.EV |
      (some e1.map and some e2.map) implies
      ((e1 -> e2 in X.sb) iff (map[e1] -> map[e2] in X'.sb))

    X.ad =   map.((X'.EV - L) <: (X'.ad)   :> (X'.EV - L)).~map
    X.cd =   map.((X'.EV - L) <: (X'.cd)   :> (X'.EV - L)).~map
    X.dd =   map.((X'.EV - L) <: (X'.dd)   :> (X'.EV - L)).~map
    X.atom = map.((X'.EV - L) <: (X'.atom) :> (X'.EV - L)).~map
    X.rf =   map.((X'.EV - L) <: (X'.rf)   :> (X'.EV - L)).~map
    X.co =   map.((X'.EV - L) <: (X'.co)   :> (X'.EV - L)).~map

    X.R     = (X'.R     - L).~map
    X.W     = (X'.W     - L).~map
    X.F     = (X'.F     - L).~map
    X.DMBST = (X'.DMBST - L).~map
    X.DMBLD = (X'.DMBLD - L).~map
    X.ISB   = (X'.ISB   - L).~map
    X.SCACQ = (X'.SCACQ - L).~map
    X.SCREL = (X'.SCREL - L).~map 

    // lock-related events in X' are on the same location
    X'.sloc = (L -> L) + ((X'.EV - L) <: ~map.(X.sloc).map :> (X'.EV - L))

    // non-call events map to non-library events
    all e : X.EV - X.LkT - X.LkN - X.UkT - X.UkN {
	  one e.map
    }

    // lock() to be transactionalised
	all e : X.LkT | some e1 : X'.EV {
      e.map = e1
      e1 in X'.R - X'.SCACQ // e1 is a lock-related read event
	  e1 not in ran[X'.rf] // e1 sees the lock is not taken
    }

	// unlock() to be transactionalised
    all e : X.UkT | no e.map

    // lock() to be kept as a normal lock
    all e : X.LkN | some disj e1, e2 : X'.EV {
      e.map = e1 + e2
      (e1 -> e2) in imm[X'.sb] & X'.atom // e1 and e2 form an RMW pair 
      e1 in X'.SCACQ & X'.R // e1 is a lock-related acquire read
      e2 in X'.W // e2 is a lock-related write
    }

    // unlock() to be kept as a normal unlock
    all e : X.UkN | some e1 : X'.EV {
 	  e.map = e1
      e1 in X'.SCREL & X'.W // eL is a lock-related release write
    }

  }   
}

pred consistent_critical_sections[X:Exec_Arm8L] {
  // no (po|com)-cycles among critical sections
  let com = X.rf + X.co + fr[none->none,X] |
  let scs = scst[X] + scsl[X] |<commit_msg>Making lock-elision bug search more general (the transaction need not see the initial value of lock -- it may now see any value of the lock variable except one set by a lock() method).<commit_after>open ../archs/exec_arm8L[E]
open ../models/aarch64_txn[E] as M

module arm8_lock_elision[E]

pred apply_map[X,X':Exec_Arm8L, map:E->E] { 

  map in (X.EV one-> X'.EV)

  // no critical sections remain
  no X'.(LkT + UkT + LkN + UkN)

  // suppose we don't have transactions in the source program
  no X.stxn

  // events in the same critical section (where the critical
  // section is one that is to be transactionalised), map to events 
  // in the same transaction.
  (X.EV - X.UkT) <: scst[X] :> (X.EV - X.UkT) = map.(X'.stxn).~map

  // the set of lock-related events introduced by the mapping
  let L = map[X.(LkT + UkT + LkN + UkN)] {

    // Mildly interesting observation: transactional memory models
    // are not monotonic w.r.t. adding sequencing edges

    X'.sthd = ~map.(X.sthd).map

    all e1, e2 : X.EV |
      (some e1.map and some e2.map) implies
      ((e1 -> e2 in X.sb) iff (map[e1] -> map[e2] in X'.sb))

    X.ad =   map.((X'.EV - L) <: (X'.ad)   :> (X'.EV - L)).~map
    X.cd =   map.((X'.EV - L) <: (X'.cd)   :> (X'.EV - L)).~map
    X.dd =   map.((X'.EV - L) <: (X'.dd)   :> (X'.EV - L)).~map
    X.atom = map.((X'.EV - L) <: (X'.atom) :> (X'.EV - L)).~map
    X.rf =   map.((X'.EV - L) <: (X'.rf)   :> (X'.EV - L)).~map
    X.co =   map.((X'.EV - L) <: (X'.co)   :> (X'.EV - L)).~map

    X.R     = (X'.R     - L).~map
    X.W     = (X'.W     - L).~map
    X.F     = (X'.F     - L).~map
    X.DMBST = (X'.DMBST - L).~map
    X.DMBLD = (X'.DMBLD - L).~map
    X.ISB   = (X'.ISB   - L).~map
    X.SCACQ = (X'.SCACQ - L).~map
    X.SCREL = (X'.SCREL - L).~map 

    // lock-related events in X' are on the same location
    X'.sloc = (L -> L) + ((X'.EV - L) <: ~map.(X.sloc).map :> (X'.EV - L))

    // non-call events map to non-library events
    all e : X.EV - X.LkT - X.LkN - X.UkT - X.UkN {
	  one e.map
    }

    // lock() to be transactionalised
	all e : X.LkT | some e1 : X'.EV {
      e.map = e1
      e1 in X'.R - X'.SCACQ // e1 is a lock-related read event
	  //e1 not in ran[X'.rf] // e1 sees the lock is not taken
    }

    // the transaction must not read a write that acquires the lock
    no X.LkN <: map.(X'.rf).~map :> X.LkT

	// unlock() to be transactionalised
    all e : X.UkT | no e.map

    // lock() to be kept as a normal lock
    all e : X.LkN | some disj e1, e2 : X'.EV {
      e.map = e1 + e2
      (e1 -> e2) in imm[X'.sb] & X'.atom // e1 and e2 form an RMW pair 
      e1 in X'.SCACQ & X'.R // e1 is a lock-related acquire read
      e2 in X'.W // e2 is a lock-related write
    }

    // unlock() to be kept as a normal unlock
    all e : X.UkN | some e1 : X'.EV {
 	  e.map = e1
      e1 in X'.SCREL & X'.W // eL is a lock-related release write
    }

  }   
}

pred consistent_critical_sections[X:Exec_Arm8L] {
  // no (po|com)-cycles among critical sections
  let com = X.rf + X.co + fr[none->none,X] |
  let scs = scst[X] + scsl[X] |
{'fraction_non_alphanumeric': 0.18669600541638456, 'fraction_numerical': 0.011848341232227487, 'mean_word_length': 1.8796296296296295, 'pattern_counts': {'":': 0, '<': 20, '<?xml version=': 0, '>': 34, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3688398', 'n_tokens_mistral': 2555, 'n_tokens_neox': 2466, 'n_words': 727}