Module RacerDDomain.ThreadsDomain

Abstraction of threads that may run in parallel with the current thread. NoThread < AnyThreadExceptSelf < AnyThread

type t =
  1. | NoThread
    (*

    No threads can run in parallel with the current thread (concretization: empty set). We assume this by default unless we see evidence to the contrary (annotations, use of locks, etc.)

    *)
  2. | AnyThreadButSelf
    (*

    Current thread can run in parallel with other threads, but not with a copy of itself. (concretization : { t | t \in TIDs && t != t_cur })

    *)
  3. | AnyThread
    (*

    Current thread can run in parallel with any thread, including itself (concretization: set of all TIDs )

    *)
val can_conflict : t -> t -> bool

return true if two accesses with these thread values can run concurrently

val is_any : t -> bool