You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

Josh Berdine 268015fbf3 [sledge] Add concurrency analysis ... Summary: This diff changes the analysis exploration algorithm from considering only sequential executions to considering executions of the interleaving semantics. As part of this, symbolic states are changed so that each thread has its own registers, while all memory is shared between them. Currently only a simple threads interface is supported: they can be created with `thread_create(&thread_routine)`, they can exit by returning from `thread_routine`, and they can be joined with `thread_join`. Current simplifications include that newly created threads are already runnable, thread routines accept no arguments and return no result, and no failures are possible. The concurrent exploration algorithm gives preference to executions which have fewer context switches, thereby performing an incremental form of context-bounded analysis. A form of partial-order reduction is performed, where the symbolic states are joined across (prefixes of) executions with the same number of context switches which reach a point where the instruction pointers and call stacks of all threads are the same. This has the effect of "dagifying" the concurrent execution tree by merging points after e.g. threads perform actions that commute with each other. This is unlike traditional partial-order reduction in that it relies on the symbolic join to combine the results of commuting operations in a way that the following symbolic execution can take advantage of, rather than performing some up-front analysis to identify commuting operations and quotienting the space of executions. The current state of the symbolic join and execution is significantly suboptimal in this regard. Differential Revision: D29441149 fbshipit-source-id: cf801a6b1		3 years ago
..
config.ml	[sledge] Make reading config file more robust	4 years ago
config.mli	[sledge] Build: Rename bin dir to cli	4 years ago
domain_itv.ml	[sledge] Add concurrency analysis	3 years ago
domain_itv.mli	[sledge] Rename Dom to Domain	4 years ago
frontend.ml	[sledge] Make tracing more explicit by including module names	4 years ago
frontend.mli	[sledge] Remove functionality depending on Llvm_linker.link_in	4 years ago
link_bc	[sledge] Add script to link bitcode using gllvm	4 years ago
sledge_buck.ml	[sledge] Remove functionality depending on Llvm_linker.link_in	4 years ago
sledge_buck.mli	[sledge] Remove functionality depending on Llvm_linker.link_in	4 years ago
sledge_cli.ml	[sledge] Add scheduler strategy for random path sampling	4 years ago
sledge_cli.mli	[sledge] Build: Rename bin dir to cli	4 years ago
smtlib.ml	[sledge] Simplify Var by combining `program` and `identified` variables	4 years ago
smtlib.mli	[sledge] Build: Rename bin dir to cli	4 years ago
version.ml	[sledge] Avoid ocamlformat regression	4 years ago
version.mli	[sledge] Build: Rename bin dir to cli	4 years ago