From 8df1f12213d4345f2bd84e5cdd5b1f5c7a265bf0 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Tue, 6 Oct 2020 05:08:19 -0700 Subject: [PATCH] [starvation] make simultaneous lock acquisition an atomic event Summary: `std::lock(x,y,z)` simultaneously acquires locks `x,y,z` in a deadlock free manner (essentially an unspecified fixed order). Starvation currently deals with it by exploiting properties of the state domain. It's a map from locks to number of times the lock is held, so the count of many locks can be increased at the same time without recording any particular lock order. In upcoming diffs the domain will be refactored into a tree of nested lock acquisitions (for other reasons) and that domain necessarily records lock order. The obvious way of doing this correctly is to allow `std::lock` as an atomic even (ie, without trying to break it into multiple acquisitions). This diff does exactly that, by changing the `Event.LockAcquire` variant to take a list of locks. Reviewed By: ezgicicek Differential Revision: D24052304 fbshipit-source-id: 410c812d7 --- infer/src/backend/StarvationGlobalAnalysis.ml | 19 +- infer/src/concurrency/starvation.ml | 77 +++++---- infer/src/concurrency/starvationDomain.ml | 163 +++++++++--------- infer/src/concurrency/starvationDomain.mli | 8 +- 4 files changed, 139 insertions(+), 128 deletions(-) diff --git a/infer/src/backend/StarvationGlobalAnalysis.ml b/infer/src/backend/StarvationGlobalAnalysis.ml index ae3ec3db5..8f71cd776 100644 --- a/infer/src/backend/StarvationGlobalAnalysis.ml +++ b/infer/src/backend/StarvationGlobalAnalysis.ml @@ -75,15 +75,16 @@ let report exe_env work_set = tenv pattrs pair acc in match pair.elem.event with - | LockAcquire lock -> - let should_report_starvation = - CriticalPair.is_uithread pair && not (Procname.is_constructor procname) - in - WorkHashSet.fold - (fun (other_procname, (other_pair : CriticalPair.t)) () acc -> - Starvation.report_on_parallel_composition ~should_report_starvation tenv pattrs - pair lock other_procname other_pair acc ) - work_set acc + | LockAcquire locks -> + List.fold locks ~init:acc ~f:(fun acc lock -> + let should_report_starvation = + CriticalPair.is_uithread pair && not (Procname.is_constructor procname) + in + WorkHashSet.fold + (fun (other_procname, (other_pair : CriticalPair.t)) () acc -> + Starvation.report_on_parallel_composition ~should_report_starvation tenv + pattrs pair lock other_procname other_pair acc ) + work_set acc ) | _ -> acc ) in diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 67852b358..365fb3fb9 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -605,12 +605,12 @@ let should_report_deadlock_on_current_proc current_elem endpoint_elem = (* should never happen *) L.die InternalError "Deadlock cannot occur without two lock events: %a" CriticalPair.pp current_elem - | LockAcquire endpoint_lock, LockAcquire current_lock -> ( + | LockAcquire endpoint_locks, LockAcquire current_locks -> ( (* first elem is a class object (see [lock_of_class]), so always report because the reverse ordering on the events will not occur since we don't search the class for static locks *) - Lock.is_class_object endpoint_lock + List.exists ~f:Lock.is_class_object endpoint_locks || - match Lock.compare_wrt_reporting endpoint_lock current_lock with + match List.compare Lock.compare_wrt_reporting endpoint_locks current_locks with | 0 -> Location.compare current_elem.CriticalPair.loc endpoint_elem.CriticalPair.loc < 0 | c -> @@ -692,17 +692,19 @@ let report_on_parallel_composition ~should_report_starvation tenv pattrs pair lo in let ltr, loc = make_trace_and_loc () in ReportMap.add_starvation High tenv pattrs loc ltr error_message report_map - | LockAcquire other_lock - when CriticalPair.may_deadlock tenv pair other_pair - && should_report_deadlock_on_current_proc pair other_pair -> - let error_message = - Format.asprintf - "Potential deadlock. %a (Trace 1) and %a (Trace 2) acquire locks %a and %a in reverse \ - orders." - pname_pp pname pname_pp other_pname Lock.describe lock Lock.describe other_lock - in - let ltr, loc = make_trace_and_loc () in - ReportMap.add_deadlock tenv pattrs loc ltr error_message report_map + | LockAcquire _ -> ( + match CriticalPair.may_deadlock tenv ~lhs:pair ~lhs_lock:lock ~rhs:other_pair with + | Some other_lock when should_report_deadlock_on_current_proc pair other_pair -> + let error_message = + Format.asprintf + "Potential deadlock. %a (Trace 1) and %a (Trace 2) acquire locks %a and %a in \ + reverse orders." + pname_pp pname pname_pp other_pname Lock.describe lock Lock.describe other_lock + in + let ltr, loc = make_trace_and_loc () in + ReportMap.add_deadlock tenv pattrs loc ltr error_message report_map + | _ -> + report_map ) | _ -> report_map else report_map @@ -751,26 +753,33 @@ let report_on_pair ~analyze_ondemand tenv pattrs (pair : Domain.CriticalPair.t) let loc = CriticalPair.get_earliest_lock_or_call_loc ~procname:pname pair in let ltr = CriticalPair.make_trace pname pair in ReportMap.add_lockless_violation tenv pattrs loc ltr error_message report_map - | LockAcquire lock when Acquisitions.lock_is_held lock pair.elem.acquisitions -> - let error_message = - Format.asprintf "Potential self deadlock. %a%a twice." pname_pp pname Lock.pp_locks lock - in - let loc = CriticalPair.get_earliest_lock_or_call_loc ~procname:pname pair in - let ltr = CriticalPair.make_trace ~header:"In method " pname pair in - ReportMap.add_deadlock tenv pattrs loc ltr error_message report_map - | LockAcquire lock when not Config.starvation_whole_program -> - Lock.root_class lock - |> Option.value_map ~default:report_map ~f:(fun other_class -> - (* get the class of the root variable of the lock in the lock acquisition - and retrieve all the summaries of the methods of that class; - then, report on the parallel composition of the current pair and any pair in these - summaries that can indeed run in parallel *) - fold_reportable_summaries analyze_ondemand tenv other_class ~init:report_map - ~f:(fun acc (other_pname, {critical_pairs}) -> - CriticalPairs.fold - (report_on_parallel_composition ~should_report_starvation tenv pattrs pair lock - other_pname) - critical_pairs acc ) ) + | LockAcquire locks -> ( + match + List.find locks ~f:(fun lock -> Acquisitions.lock_is_held lock pair.elem.acquisitions) + with + | Some lock -> + let error_message = + Format.asprintf "Potential self deadlock. %a%a twice." pname_pp pname Lock.pp_locks lock + in + let loc = CriticalPair.get_earliest_lock_or_call_loc ~procname:pname pair in + let ltr = CriticalPair.make_trace ~header:"In method " pname pair in + ReportMap.add_deadlock tenv pattrs loc ltr error_message report_map + | None when Config.starvation_whole_program -> + report_map + | None -> + List.fold locks ~init:report_map ~f:(fun acc lock -> + Lock.root_class lock + |> Option.value_map ~default:acc ~f:(fun other_class -> + (* get the class of the root variable of the lock in the lock acquisition + and retrieve all the summaries of the methods of that class; + then, report on the parallel composition of the current pair and any pair in these + summaries that can indeed run in parallel *) + fold_reportable_summaries analyze_ondemand tenv other_class ~init:acc + ~f:(fun acc (other_pname, {critical_pairs}) -> + CriticalPairs.fold + (report_on_parallel_composition ~should_report_starvation tenv pattrs pair + lock other_pname) + critical_pairs acc ) ) ) ) | _ -> report_map diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 487d65cc3..af53f651e 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -107,6 +107,24 @@ module Lock = struct let mk_str t = root_class t |> Option.value_map ~default:"" ~f:Typ.Name.to_string in (* use string comparison on types as a stable order to decide whether to report a deadlock *) String.compare (mk_str t1) (mk_str t2) + + + let apply_subst_to_list subst l = + let rec apply_subst_to_list_inner l = + match l with + | [] -> + ([], false) + | lock :: locks -> ( + let locks', modified = apply_subst_to_list_inner locks in + match apply_subst subst lock with + | None -> + (locks', true) + | Some lock' when (not modified) && phys_equal lock lock' -> + (l, false) + | Some lock' -> + (lock' :: locks', true) ) + in + apply_subst_to_list_inner l |> fst end module AccessExpressionDomain = struct @@ -159,15 +177,15 @@ end module Event = struct type t = - | LockAcquire of Lock.t + | LockAcquire of Lock.t list | MayBlock of (Procname.t * StarvationModels.severity) | StrictModeCall of Procname.t | MonitorWait of Lock.t [@@deriving compare] let pp fmt = function - | LockAcquire lock -> - F.fprintf fmt "LockAcquire(%a)" Lock.pp lock + | LockAcquire locks -> + F.fprintf fmt "LockAcquire(%a)" (PrettyPrintable.pp_collection ~pp_item:Lock.pp) locks | MayBlock (pname, sev) -> F.fprintf fmt "MayBlock(%a, %a)" Procname.pp pname StarvationModels.pp_severity sev | StrictModeCall pname -> @@ -178,8 +196,8 @@ module Event = struct let describe fmt elem = match elem with - | LockAcquire lock -> - Lock.pp_locks fmt lock + | LockAcquire locks -> + Pp.comma_seq Lock.pp_locks fmt locks | MayBlock (pname, _) | StrictModeCall pname -> F.fprintf fmt "calls %a" describe_pname pname | MonitorWait lock -> @@ -195,24 +213,20 @@ module Event = struct let make_object_wait lock = MonitorWait lock let apply_subst subst event = - let make_monitor_wait lock = MonitorWait lock in - let make_lock_acquire lock = LockAcquire lock in - let apply_subst_aux make lock = - match Lock.apply_subst subst lock with - | None -> - None - | Some lock' when phys_equal lock lock' -> - Some event - | Some lock' -> - Some (make lock') - in match event with - | MonitorWait lock -> - apply_subst_aux make_monitor_wait lock - | LockAcquire lock -> - apply_subst_aux make_lock_acquire lock | MayBlock _ | StrictModeCall _ -> Some event + | MonitorWait lock -> + Lock.apply_subst subst lock + |> Option.map ~f:(fun lock' -> if phys_equal lock lock' then event else MonitorWait lock') + | LockAcquire locks -> ( + match Lock.apply_subst_to_list subst locks with + | [] -> + None + | locks' when phys_equal locks locks' -> + Some event + | locks' -> + Some (LockAcquire locks') ) end (** A lock acquisition with source location and procname in which it occurs. The location & procname @@ -275,8 +289,6 @@ module LockState : sig val release : Lock.t -> t -> t - val is_lock_taken : Event.t -> t -> bool - val get_acquisitions : t -> Acquisitions.t end = struct (* abstraction limit for lock counts *) @@ -316,14 +328,6 @@ end = struct let is_top {map} = Map.is_top map - let is_lock_taken event {acquisitions} = - match event with - | Event.LockAcquire lock -> - Acquisitions.mem (Acquisition.make_dummy lock) acquisitions - | _ -> - false - - let acquire ~procname ~loc lock {map; acquisitions} = let should_add_acquisition = ref false in let map = @@ -399,9 +403,10 @@ let is_recursive_lock event tenv = (Typ.pp_full Pp.text) typ ; true in - match event with - | Event.LockAcquire lock_path -> - Lock.get_typ tenv lock_path |> Option.exists ~f:is_class_and_recursive_lock + match (event : Event.t) with + | LockAcquire locks -> + List.exists locks ~f:(fun lock_path -> + Lock.get_typ tenv lock_path |> Option.exists ~f:is_class_and_recursive_lock ) | _ -> false @@ -413,19 +418,19 @@ module CriticalPair = struct let is_blocking_call {elem= {event}} = match event with LockAcquire _ -> true | _ -> false - let get_final_acquire {elem= {event}} = - match event with LockAcquire lock -> Some lock | _ -> None - - - let may_deadlock tenv ({elem= pair1} as t1 : t) ({elem= pair2} as t2 : t) = - ThreadDomain.can_run_in_parallel pair1.thread pair2.thread - && Option.both (get_final_acquire t1) (get_final_acquire t2) - |> Option.exists ~f:(fun (lock1, lock2) -> - (not (Lock.equal_across_threads tenv lock1 lock2)) - && Acquisitions.lock_is_held_in_other_thread tenv lock2 pair1.acquisitions - && Acquisitions.lock_is_held_in_other_thread tenv lock1 pair2.acquisitions - && Acquisitions.no_locks_common_across_threads tenv pair1.acquisitions - pair2.acquisitions ) + let may_deadlock tenv ~(lhs : t) ~lhs_lock ~(rhs : t) = + let get_acquired_locks {elem= {event}} = + match event with LockAcquire locks -> locks | _ -> [] + in + if ThreadDomain.can_run_in_parallel lhs.elem.thread rhs.elem.thread then + get_acquired_locks rhs + |> List.find ~f:(fun rhs_lock -> + (not (Lock.equal_across_threads tenv lhs_lock rhs_lock)) + && Acquisitions.lock_is_held_in_other_thread tenv rhs_lock lhs.elem.acquisitions + && Acquisitions.lock_is_held_in_other_thread tenv lhs_lock rhs.elem.acquisitions + && Acquisitions.no_locks_common_across_threads tenv lhs.elem.acquisitions + rhs.elem.acquisitions ) + else None let apply_subst subst pair = @@ -436,26 +441,34 @@ module CriticalPair = struct Some (map ~f:(fun _elem -> elem') pair) + (** if given [Some tenv], transform a pair so as to remove reentrant locks that are already in + [held_locks] *) + let filter_out_reentrant_relocks tenv_opt held_locks pair = + match (tenv_opt, pair.elem.event) with + | Some tenv, LockAcquire locks -> ( + let filtered_locks = + IList.filter_changed locks ~f:(fun lock -> + (not (Acquisitions.lock_is_held lock held_locks)) + || not (is_recursive_lock pair.elem.event tenv) ) + in + match filtered_locks with + | [] -> + None + | _ when phys_equal filtered_locks locks -> + Some pair + | _ -> + Some (map pair ~f:(fun elem -> {elem with event= LockAcquire filtered_locks})) ) + | _, _ -> + Some pair + + let integrate_summary_opt ?subst ?tenv existing_acquisitions call_site (caller_thread : ThreadDomain.t) (callee_pair : t) = let substitute_pair subst callee_pair = match subst with None -> Some callee_pair | Some subst -> apply_subst subst callee_pair in - let filter_out_reentrant_relock callee_pair = - match tenv with - | None -> - Some callee_pair - | Some tenv - when get_final_acquire callee_pair - |> Option.for_all ~f:(fun lock -> - (not (Acquisitions.lock_is_held lock existing_acquisitions)) - || not (is_recursive_lock callee_pair.elem.event tenv) ) -> - Some callee_pair - | _ -> - None - in substitute_pair subst callee_pair - |> Option.bind ~f:filter_out_reentrant_relock + |> Option.bind ~f:(filter_out_reentrant_relocks tenv existing_acquisitions) |> Option.bind ~f:(fun callee_pair -> ThreadDomain.apply_to_pair caller_thread callee_pair.elem.thread |> Option.map ~f:(fun thread -> @@ -528,17 +541,6 @@ module CriticalPair = struct let can_run_in_parallel t1 t2 = ThreadDomain.can_run_in_parallel t1.elem.thread t2.elem.thread end -(** skip adding an order pair [(_, event)] if - - - we have no tenv, or, - - [event] is not a lock event, or, - - we do not hold the lock, or, - - the lock is not recursive. *) -let should_skip ?tenv event lock_state = - Option.exists tenv ~f:(fun tenv -> - LockState.is_lock_taken event lock_state && is_recursive_lock event tenv ) - - module CriticalPairs = struct include CriticalPair.FiniteSet @@ -548,9 +550,8 @@ module CriticalPairs = struct (fun critical_pair acc -> CriticalPair.integrate_summary_opt ?subst ?tenv existing_acquisitions call_site thread critical_pair - |> Option.fold ~init:acc ~f:(fun acc (new_pair : CriticalPair.t) -> - if should_skip ?tenv new_pair.elem.event lock_state then acc else add new_pair acc ) - ) + |> Option.bind ~f:(CriticalPair.filter_out_reentrant_relocks tenv existing_acquisitions) + |> Option.value_map ~default:acc ~f:(fun new_pair -> add new_pair acc) ) astate empty end @@ -691,19 +692,17 @@ let leq ~lhs ~rhs = let add_critical_pair ?tenv lock_state event thread ~loc acc = - if should_skip ?tenv event lock_state then acc - else - let acquisitions = LockState.get_acquisitions lock_state in - let critical_pair = CriticalPair.make ~loc acquisitions event thread in - CriticalPairs.add critical_pair acc + let acquisitions = LockState.get_acquisitions lock_state in + let critical_pair = CriticalPair.make ~loc acquisitions event thread in + CriticalPair.filter_out_reentrant_relocks tenv acquisitions critical_pair + |> Option.value_map ~default:acc ~f:(fun pair -> CriticalPairs.add pair acc) let acquire ?tenv ({lock_state; critical_pairs} as astate) ~procname ~loc locks = { astate with critical_pairs= - List.fold locks ~init:critical_pairs ~f:(fun acc lock -> - let event = Event.make_acquire lock in - add_critical_pair ?tenv lock_state event astate.thread ~loc acc ) + (let event = Event.make_acquire locks in + add_critical_pair ?tenv lock_state event astate.thread ~loc critical_pairs ) ; lock_state= List.fold locks ~init:lock_state ~f:(fun acc lock -> LockState.acquire ~procname ~loc lock acc ) } diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index c5807945f..3682f22cd 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -57,7 +57,7 @@ end module Event : sig type t = - | LockAcquire of Lock.t + | LockAcquire of Lock.t list | MayBlock of (Procname.t * StarvationModels.severity) | StrictModeCall of Procname.t | MonitorWait of Lock.t @@ -107,8 +107,10 @@ module CriticalPair : sig val get_earliest_lock_or_call_loc : procname:Procname.t -> t -> Location.t (** outermost callsite location OR lock acquisition *) - val may_deadlock : Tenv.t -> t -> t -> bool - (** two pairs can run in parallel and satisfy the conditions for deadlock *) + val may_deadlock : Tenv.t -> lhs:t -> lhs_lock:Lock.t -> rhs:t -> Lock.t option + (** if two pairs can run in parallel and satisfy the conditions for deadlock, when [lhs_lock] of + [lhs] is involved return the lock involved from [rhs], as [LockAcquire] may involve more than + one *) val make_trace : ?header:string -> ?include_acquisitions:bool -> Procname.t -> t -> Errlog.loc_trace