[SV-COMP'18 5/19] Abort concurrency encoding in possibly unsound cases #1994
Conversation
src/goto-symex/goto_symex_state.cpp
Outdated
| @@ -342,6 +342,9 @@ void goto_symex_statet::assignment( | |||
| assert_l2_renaming(lhs); | |||
| assert_l2_renaming(rhs); | |||
|
|
|||
| if(is_shared && lhs.type().id() == ID_pointer) | |||
There was a problem hiding this comment.
Add a comment here referencing an issue that describes what's wrong, and what we'd need to do to fix it.
tautschnig
force-pushed
the
concurrency-soundness
branch
from
d66faf0 to
cffae65
Compare
tautschnig
force-pushed
the
concurrency-soundness
branch
from
cffae65 to
26b13ae
Compare
| @@ -342,6 +342,10 @@ void goto_symex_statet::assignment( | |||
| assert_l2_renaming(lhs); | |||
| assert_l2_renaming(rhs); | |||
|
|
|||
| // see #305 on GitHub for a simple example and possible discussion | |||
| if(is_shared && lhs.type().id() == ID_pointer) | |||
| throw "pointer handling for concurrency is unsound"; | |||
There was a problem hiding this comment.
Note: that should be turned into a user facing exception (not an invariant) during the error handling clean up.
|
@peterschrammel @tautschnig In Java everything is a pointer, which means that pretty much nothing works after this if the program is multithreaded. In particular all tests in the about-to-be-merged #2280 now break. We should have been told about this. I do support the move to make the user aware that pointer reasoning in a multithread environment is currently unsound. But this means that our work since September 2017 on Java concurrency is unusable after this. The solution is obviously fixing symex, but that will take a while and we have now new priorities. What about just emitting a warning instead of throwing? |
This PR has been public for a fair while, so I'm not sure what else should have been said? Are there reasons that symex is actually sound for Java, despite the limitations? If so, maybe we can tweak the check here to accept the cases where it is sound. The key question for the current implementation being sound is whether a pointer will always be set/updated by a thread with a lower thread id before it is being dereferenced in a thread with the same or a higher thread id. |
|
I cannot imagine any such reason. Java threads can access global variables (static fields) in any possible order, like POSIX threads. Again, what's the reason for aborting? BMC is in general unsound, and CBMC is probably unsound in some other aspects other than loop bounding. The user is aware of it and can live with it. What's the point of aborting instead of emitting a warning? |
I'm not sure I agree with this: BMC isn't unsound per se if you use loop unwinding assertions, let alone for loop-free programs. The other sources of unsoundness in CBMC, apart from existing-but-not-yet-known bugs, are step-by-step being removed - in fact #1086 is the only other remaining one that I am aware of. So the point is indeed being sound. Please do push back on the above, I might as well be wrong. Otherwise I'd also be happy to have a command-line option that allows skipping this soundness-check (much like not enabling --unwinding-assertions also takes you into unsound territory). Command-line options enable to user to make a conscious choice. |
|
I do support the move of making the tool as sound as possible, and even making that the default when it's possible. But that has to be balanced with the fact that development is done step by step and people has different priorities. What about not throwing (and instead showing a warning) when Not making this throw a warning (conditional on the presence of a commandline option or by default) makes impossible to continue adding support for concurrency in Java in places other than fixing the very problem that this throw points out. |
|
I'd happily approve a pull request that adds an option which |
e6d196d Merge pull request diffblue#2355 from owen-jones-diffblue/owen-jones-diffblue/add-name-to-array-type 6f7580d Merge pull request diffblue#2351 from romainbrenguier/bugfix/null-array b2089b7 Add unit test for array_poolt 2df6d81 Set name of java array types 50e02b0 Simplify make_char_array_for_char_pointer 645eda9 Improve invariant message 3c7a671 Look up for null pointer in array pool 32a4186 Merge pull request diffblue#2302 from romainbrenguier/refactor/ci-lazy-methods c4aadab Extract handle_virtual_methods_with_no_callees cac016d Extract a convert_and_analyze_method method ca0adc9 Correct indentation 24b6936 Extract entry_point_methods method 360fabe Merge pull request diffblue#2356 from peterschrammel/fix-goto-simplification 4394016 Temporary fix to enable if-then-else simplifications d433438 Test for if-then-else optimisation in goto convert e5d1c12 Merge pull request diffblue#2354 from Degiorgio/disable-soundness-check-for-shared-pointers 7d4d4bd Skip check for unsoundness in shared pointer handling (java only) 8e6244c Merge pull request diffblue#2043 from peterschrammel/fail-on-uncaught-exception ec3010f Merge pull request diffblue#1994 from tautschnig/concurrency-soundness 1a9850a Merge pull request diffblue#2326 from tautschnig/c++-enum b71efaf Merge pull request diffblue#2019 from tautschnig/remove-unused 26b13ae Abort concurrency encoding in possibly unsound cases cd2ef4b Enable throwing of AssertionError 653d887 Remove wrong assumption from goto check 07acde4 Refactor user-defined assertion translation for Java 04c0205 Assert that there is uncaught exception 1daf466 Use resolver to translate cpp_name to scoped base_name 471b20f Remove prop_assignmentt interface 2639cf1 Remove unused solvers/prop/prop_conv_store.{h,cpp} 502687e Remove unused solver/prop/prop_wrapper.h ae56978 Remove unused goto-analyzer/static_analyzer.{h,cpp} 2260f82 Remove path_accelerationt interface d350e5c Remove unused nondet_ifthenelse.{h,cpp} a4936f8 Remove unused cpp/recursion_counter.h 71cfbbd Remove unused sorted_vector.h 4d4c9c6 Revert "added pipe_stream class" 2696420 Revert "new exception class" 3fb06ba Revert "Added utility class to convert strings into expressions" 55bdbc7 Recompile regression test class files 118f41f Merge pull request diffblue#2352 from tautschnig/c++-auto-tc 5a4dc8d Merge pull request diffblue#2315 from diffblue/fix-goto 199d4cc prevent half-constructed GOTO instructions 72156d5 C++ front-end: fix auto+references after already-typechecked cleanup 8fac5ed Merge pull request diffblue#2069 from romainbrenguier/refactor/convert_instruction 309d207 remove conversion for non-deterministic-goto 67081d5 Extract convert_pop function cd98a1f Extract convert_switch function f2acb00 Extract convert_dup2_x2 function 66cf709 Extract convert_dup2_x1 function e0735af Extract convert_dup2 function 51f53ca Extract convert_const function d627638 Extract convert_invoke function fcfca08 Extract replace_calls_to_cprover_assume function 0a521a4 Extract convert_checkcast function 4c28f99 Extract convert_athrow function 21e37a8 Extract convert_monitorexit function a7bbf53 Extract do_exception_handling function 0aa1c8e Extract convert_monitorenter function 48dd97f Extract convert_multianewarray function edc4a28 Extract convert_newarray function f8d00f6 Extract convert_new function b846798 Extract convert_putstatic function 27af4a2 Extract convert_putfield function f1edff9 Extract convert_getstatic function 68bddf1 Remove redundant assert 6f0f3fb Extract convert_cmp2 function 3049281 Extract convert_cmp function 5a5788c Extract convert_ushr function 305ede8 Extract convert_iinc function 61d03da Extract convert_ifnull function b4f6d04 Extract convert_if_nonull function 0e911d4 Extract convert_if function 651246e Extract convert_if_cmp function fc95df1 Extract convert_ret function ce58dca Extract convert_aload/store/astore functions 14e3c35 Extract convert_invokedynamic function 939bb53 Rename iterators and use auto ddb31a0 Extract draw_edges_from_ret_to_jsr function 390063f Extract try_catch_handler function 87a4f31 Make label static 36ed947 Replace assert by invariant 036f1b1 Use auto for iterator types git-subtree-dir: cbmc git-subtree-split: e6d196d
No description provided.