Skip to content

Klever concurrency safety support #688

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
sim642 merged 9 commits into from
Jan 9, 2024
Merged

Klever concurrency safety support #688

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
d754d76
Add direct Klever concurrency specials
sim642 Apr 13, 2022
8f31609
Add special rtnl_lock from Linux
sim642 Apr 13, 2022
1fbf910
Add symb_locks to ldv-races conf
sim642 Apr 13, 2022
edf7e6f
Merge branch 'master' into klever
sim642 Nov 27, 2023
717b6a8
Add pthread_join_N to Klever library
sim642 Nov 27, 2023
670e7cf
Add test for Klever's multiple threads
sim642 Nov 27, 2023
8a95c8a
Add multiple flag to ThreadCreate
sim642 Nov 27, 2023
5a6362e
Fix LibraryDslTest compilation
sim642 Nov 27, 2023
27684fe
Merge branch 'master' into klever
sim642 Jan 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion conf/ldv-races.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,9 @@
"access",
"escape",
"expRelation",
"mhp"
"mhp",
"var_eq",
"symb_locks"
],
"malloc": {
"wrappers": [
Expand Down
5 changes: 4 additions & 1 deletion src/analyses/libraryFunctions.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,8 @@ let classify' fn exps =
`Unknown fn
in
match fn with
| "pthread_create" ->
| "pthread_create"
| "pthread_create_N" -> (* Klever *)
Comment thread
sim642 marked this conversation as resolved.
Outdated
begin match exps with
| [id;_;fn;x] -> `ThreadCreate (id, fn, x)
| _ -> strange_arguments ()
Expand Down Expand Up @@ -72,6 +73,7 @@ let classify' fn exps =
| "pthread_rwlock_wrlock" | "GetResource" | "_raw_spin_lock"
| "_raw_spin_lock_flags" | "_raw_spin_lock_irqsave" | "_raw_spin_lock_irq" | "_raw_spin_lock_bh"
| "spin_lock_irqsave" | "spin_lock"
| "ldv_mutex_model_lock" | "ldv_spin_model_lock" (* Klever *)
-> `Lock (get_bool "sem.lock.fail", true, true)
| "pthread_mutex_lock" | "__pthread_mutex_lock"
-> `Lock (get_bool "sem.lock.fail", true, false)
Expand All @@ -84,6 +86,7 @@ let classify' fn exps =
| "mutex_unlock" | "ReleaseResource" | "_write_unlock" | "_read_unlock" | "_raw_spin_unlock_irqrestore"
| "pthread_mutex_unlock" | "__pthread_mutex_unlock" | "spin_unlock_irqrestore" | "up_read" | "up_write"
| "up"
| "ldv_mutex_model_unlock" | "ldv_spin_model_unlock" (* Klever *)
-> `Unlock
| x -> `Unknown x

Expand Down
15 changes: 11 additions & 4 deletions src/analyses/mutexEventsAnalysis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ open GobConfig

let big_kernel_lock = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[big kernel lock]" intType))
let console_sem = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[console semaphore]" intType))
let rtnl_lock = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[rtnl_lock]" intType))
let verifier_atomic = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[__VERIFIER_atomic]" intType))

module Spec: MCPSpec =
Expand Down Expand Up @@ -77,7 +78,8 @@ struct
let unlock remove_fn =
match f.vname, arglist with
| _, [arg]
| ("spin_unlock_irqrestore" | "_raw_spin_unlock_irqrestore"), [arg; _] ->
| ("spin_unlock_irqrestore" | "_raw_spin_unlock_irqrestore"), [arg; _]
| "ldv_mutex_model_unlock", [arg; _] -> (* Klever *)
List.iter (fun e ->
ctx.split () [Events.Unlock (remove_fn e)]
) (eval_exp_addr (Analyses.ask_of_ctx ctx) arg);
Expand All @@ -92,7 +94,8 @@ struct
| `Lock (failing, rw, nonzero_return_when_aquired), _ ->
begin match f.vname, arglist with
| _, [arg]
| "spin_lock_irqsave", [arg; _] ->
| "spin_lock_irqsave", [arg; _]
| "ldv_mutex_model_lock", [arg; _] -> (* Klever *)
(*print_endline @@ "Mutex `Lock "^f.vname;*)
lock ctx rw failing nonzero_return_when_aquired (Analyses.ask_of_ctx ctx) lv arg
| _ -> failwith "lock has multiple arguments"
Expand All @@ -116,10 +119,14 @@ struct
(*print_endline @@ "Mutex `Unlock "^f.vname;*)
unlock remove_rw
| _, "spinlock_check" -> ()
| _, "acquire_console_sem" when get_bool "kernel" ->
| _, "acquire_console_sem"-> (* TODO: removed for Klever: when get_bool "kernel" *)
ctx.emit (Events.Lock (console_sem, true))
| _, "release_console_sem" when get_bool "kernel" ->
| _, "release_console_sem" -> (* TODO: removed for Klever: when get_bool "kernel" *)
ctx.emit (Events.Unlock console_sem)
| _, "rtnl_lock"->
ctx.emit (Events.Lock (rtnl_lock, true))
| _, ("rtnl_unlock" | "__rtnl_unlock") ->
ctx.emit (Events.Unlock rtnl_lock)
| _, "__builtin_prefetch" | _, "misc_deregister" ->
()
| _, "__VERIFIER_atomic_begin" when get_bool "ana.sv-comp.functions" ->
Expand Down