Module Spec.A

ego tid * must-lockset * creation-lockset

include sig ... end
type t = TID.t * Lockset.t * G.t
val equal : t -> t -> Ppx_deriving_runtime.bool
val compare : t -> t -> Ppx_deriving_runtime.int
val hash : t -> int
val relift : t -> t
val tag : 'a -> 'b
val arbitrary : unit -> (TID.t * Lockset.t * G.t) QCheck.arbitrary
val name : unit -> string
val one_protected_inter_threaded_other_intra_threaded : G.t -> TID.t -> G.value -> bool

checks if cl1 has a mapping (tp1 |-> ls1) such that ls1 and ls2 are not disjoint and tp1 != t2

  • parameter cl1

    creation-lockset of thread t1 at first program point

  • parameter t2

    thread id at second program point

  • parameter ls2

    lockset at second program point

  • returns

    whether t1 must be running mutually exclusive with second program point

val both_protected_inter_threaded : G.t -> G.t -> bool

checks if cl1 has a member (tp1 |-> ls1) and cl2 has a member (tp2 |-> ls2) such that ls1 and ls2 are not disjoint and tp1 != tp2

  • parameter cl1

    creation-lockset of first thread t1

  • parameter cl2

    creation-lockset of second thread t2

  • returns

    whether t1 and t2 must be running mutually exclusive

val may_race : (TID.t * G.value * G.t) -> (TID.t * G.value * G.t) -> bool
val pretty : unit -> ('a * 'b * G.t) -> Printable.Pretty.doc
val show : ('a * 'b * G.t) -> string
val to_yojson : ('a * 'b * G.t) -> Yojson.Safe.t
val printXml : 'a BatInnerIO.output -> ('b * 'c * G.t) -> unit
val should_print : ('a * 'b * G.t) -> bool