Module `RacerDDomain.ThreadsDomain`

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

type t = | 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.) | 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 }) | 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
val update_for_lock_use : t -> t: update thread status when a lock instruction is observed

`\|` `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.)
`\|` `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 }`)
`\|` `AnyThread`	Current thread can run in parallel with any thread, including itself (concretization: set of all TIDs )