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		4 years ago
..
context_test.ml	[sledge] Compare Vars by id	5 years ago
context_test.mli	[sledge] Switch Fol.Context from using Ses.Equality to Context	5 years ago
fol_test.ml	[sledge] Add concurrency analysis	4 years ago
fol_test.mli	[sledge] Test: Move test modules into test directory	5 years ago
sh_test.ml	[sledge] Reimplement equality solver based on "use" superterm index	5 years ago
sh_test.mli	[sledge] Test: Move test modules into test directory	5 years ago
solver_test.ml	[sledge] Add a distinct formula and use it to strengthen Sh.pure_approx	4 years ago
solver_test.mli	[sledge] Test: Move test modules into test directory	5 years ago
term_test.ml	[sledge] Reorganize first-order logic support into separate library	5 years ago
term_test.mli	[sledge] Test: Move test modules into test directory	5 years ago