@ -177,56 +177,61 @@ end
module Event = struct
module Event = struct
type t =
type t =
| LockAcquire of Lock . t list
| LockAcquire of { locks : Lock . t list }
| MayBlock of (Procname . t * StarvationModels . severity )
| MayBlock of {callee : Procname . t ; severity : StarvationModels . severity }
| StrictModeCall of Procname . t
| StrictModeCall of { callee : Procname . t }
| MonitorWait of Lock . t
| MonitorWait of { lock : Lock . t }
[ @@ deriving compare ]
[ @@ deriving compare ]
let pp fmt = function
let pp fmt = function
| LockAcquire locks ->
| LockAcquire { locks } ->
F . fprintf fmt " LockAcquire(%a) " ( PrettyPrintable . pp_collection ~ pp_item : Lock . pp ) locks
F . fprintf fmt " LockAcquire(%a) " ( PrettyPrintable . pp_collection ~ pp_item : Lock . pp ) locks
| MayBlock (pname , sev ) ->
| MayBlock {callee ; severity } ->
F . fprintf fmt " MayBlock(%a, %a) " Procname . pp pnam e StarvationModels . pp_severity sev
F . fprintf fmt " MayBlock(%a, %a) " Procname . pp calle e StarvationModels . pp_severity sev erity
| StrictModeCall pname ->
| StrictModeCall { callee } ->
F . fprintf fmt " StrictModeCall(%a) " Procname . pp pnam e
F . fprintf fmt " StrictModeCall(%a) " Procname . pp calle e
| MonitorWait lock ->
| MonitorWait { lock } ->
F . fprintf fmt " MonitorWait(%a) " Lock . pp lock
F . fprintf fmt " MonitorWait(%a) " Lock . pp lock
let describe fmt elem =
let describe fmt elem =
match elem with
match elem with
| LockAcquire locks ->
| LockAcquire { locks } ->
Pp . comma_seq Lock . pp_locks fmt locks
Pp . comma_seq Lock . pp_locks fmt locks
| MayBlock (pname , _ ) | StrictModeCall pname ->
| MayBlock {callee } | StrictModeCall { callee } ->
F . fprintf fmt " calls %a " describe_pname pnam e
F . fprintf fmt " calls %a " describe_pname calle e
| MonitorWait lock ->
| MonitorWait { lock } ->
F . fprintf fmt " calls `wait` on %a " Lock . describe lock
F . fprintf fmt " calls `wait` on %a " Lock . describe lock
let make_acquire lock = LockAcquire lock
let make_acquire lock s = LockAcquire { lock s}
let make_blocking_call callee sev = MayBlock ( callee , sev )
let make_blocking_call callee sev erity = MayBlock { callee ; severity }
let make_strict_mode_call callee = StrictModeCall callee
let make_strict_mode_call callee = StrictModeCall { callee }
let make_object_wait lock = MonitorWait lock
let make_object_wait lock = MonitorWait { lock }
let apply_subst subst event =
let apply_subst subst event =
match event with
match event with
| MayBlock _ | StrictModeCall _ ->
| MayBlock _ | StrictModeCall _ ->
Some event
Some event
| MonitorWait lock ->
| MonitorWait { lock } -> (
Lock . apply_subst subst lock
match Lock . apply_subst subst lock with
| > Option . map ~ f : ( fun lock' -> if phys_equal lock lock' then event else MonitorWait lock' )
| None ->
| LockAcquire locks -> (
None
| Some lock' when phys_equal lock lock' ->
Some event
| Some lock ->
Some ( MonitorWait { lock } ) )
| LockAcquire { locks } -> (
match Lock . apply_subst_to_list subst locks with
match Lock . apply_subst_to_list subst locks with
| [] ->
| [] ->
None
None
| locks' when phys_equal locks locks' ->
| locks' when phys_equal locks locks' ->
Some event
Some event
| locks ' ->
| locks ->
Some ( LockAcquire locks' ) )
Some ( LockAcquire { locks } ) )
end
end
(* * A lock acquisition with source location and procname in which it occurs. The location & procname
(* * A lock acquisition with source location and procname in which it occurs. The location & procname
@ -404,7 +409,7 @@ let is_recursive_lock event tenv =
true
true
in
in
match ( event : Event . t ) with
match ( event : Event . t ) with
| LockAcquire locks ->
| LockAcquire { locks } ->
List . exists locks ~ f : ( fun lock_path ->
List . exists locks ~ f : ( fun lock_path ->
Lock . get_typ tenv lock_path | > Option . exists ~ f : is_class_and_recursive_lock )
Lock . get_typ tenv lock_path | > Option . exists ~ f : is_class_and_recursive_lock )
| _ ->
| _ ->
@ -420,7 +425,7 @@ module CriticalPair = struct
let may_deadlock tenv ~ ( lhs : t ) ~ lhs_lock ~ ( rhs : t ) =
let may_deadlock tenv ~ ( lhs : t ) ~ lhs_lock ~ ( rhs : t ) =
let get_acquired_locks { elem = { event } } =
let get_acquired_locks { elem = { event } } =
match event with LockAcquire locks -> locks | _ -> []
match event with LockAcquire { locks } -> locks | _ -> []
in
in
if ThreadDomain . can_run_in_parallel lhs . elem . thread rhs . elem . thread then
if ThreadDomain . can_run_in_parallel lhs . elem . thread rhs . elem . thread then
get_acquired_locks rhs
get_acquired_locks rhs
@ -445,7 +450,7 @@ module CriticalPair = struct
[ held_locks ] * )
[ held_locks ] * )
let filter_out_reentrant_relocks tenv_opt held_locks pair =
let filter_out_reentrant_relocks tenv_opt held_locks pair =
match ( tenv_opt , pair . elem . event ) with
match ( tenv_opt , pair . elem . event ) with
| Some tenv , LockAcquire locks -> (
| Some tenv , LockAcquire { locks } -> (
let filtered_locks =
let filtered_locks =
IList . filter_changed locks ~ f : ( fun lock ->
IList . filter_changed locks ~ f : ( fun lock ->
( not ( Acquisitions . lock_is_held lock held_locks ) )
( not ( Acquisitions . lock_is_held lock held_locks ) )
@ -456,8 +461,8 @@ module CriticalPair = struct
None
None
| _ when phys_equal filtered_locks locks ->
| _ when phys_equal filtered_locks locks ->
Some pair
Some pair
| _ ->
| locks ->
Some ( map pair ~ f : ( fun elem -> { elem with event = LockAcquire filtered_ locks} ) ) )
Some ( map pair ~ f : ( fun elem -> { elem with event = LockAcquire { locks} } ) ) )
| _ , _ ->
| _ , _ ->
Some pair
Some pair