Making the instrumented clinit_wrapper function thread-safe by Degiorgio · Pull Request #1786 · diffblue/cbmc

Degiorgio · 2018-01-31T16:20:23Z

The previous version of clinit_wrapper did not conform to the JVM specification (section 5.5) as it did not support concurrency. More specifically, the clinit_wrapper has to be carefully synchronized
as other threads may try to initialize a given class or interface at the same-time.

This commit adds a new implementation of the clinit_wrapper that is thread-safe. This is achieved by introducing a critical section and two state variables. The commit implements a simplification of the algorithm defined in section 5.5 of the JVM spec. For instance exceptions thrown during the execution of static initializers are not properly handled. To use this implementation instead of the old one, a new option has been added 'java-threading'. We made this opt-in instead of simply replacing the old one for performance reasons.

Commit duplicates some regression tests, while these tests do not exhibit concurrency, the resulting change to the clinit_wrapper trigged by specifying 'java-threading' effects non-concurrent code.

Note: this change is required in-order to add concurrency support to the java-front-end.

thk123 · 2018-01-31T16:48:15Z

. @smowton should definitely look at this as has been touching this recently, I'd also appreciate a test-gen pointer bump.

peterschrammel · 2018-02-01T11:36:15Z

src/java_bytecode/java_bytecode_convert_method.cpp

peterschrammel · 2018-02-01T11:39:22Z

src/java_bytecode/java_bytecode_convert_method.cpp

peterschrammel · 2018-02-01T13:24:56Z

src/java_bytecode/java_bytecode_convert_method.cpp

Do you require a full int here?

peterschrammel · 2018-02-01T15:09:12Z

src/java_bytecode/java_bytecode_convert_method.cpp

It might be worth factoring out the clinit generation into a separate .cpp file in order to reduce the size of this monster.cpp.

agreed, will do this.

Hang on! This is already done in the PR this is racing against :)

smowton

Some nitpicks, and some bad news: this is going to clash with #1774, which I hope to get in later today, and reworks how static init methods are generated to create them lazily, and create their state variables (the bool already_run, and now your new state variable) before method conversion.

The good news however: this should be quite easy to rebase on #1774 -- simply create your additional global where #1774 does and copy-paste your init code into my new java_static_initializers.cpp file.

The local variable should be created during method elaboration (i.e. in get_clinit_wrapper_body).

smowton · 2018-02-02T10:39:06Z

src/java_bytecode/java_bytecode_convert_method.cpp

Since this is new code, use the new clang-format-compatible / human-readable operator spacing (i.e. spaces around ==, =, etc)

smowton · 2018-02-02T10:40:19Z

src/java_bytecode/java_bytecode_convert_method.cpp

Consider making a std_code entry for these?

smowton · 2018-02-02T10:41:59Z

src/java_bytecode/java_bytecode_convert_method.cpp

smowton · 2018-02-02T10:42:19Z

src/java_bytecode/java_bytecode_convert_method.cpp

smowton · 2018-02-02T10:44:20Z

src/java_bytecode/java_bytecode_convert_method.cpp

Generally base_name is the unqualified name, e.g. name == java::Class.field => base_name == field.

smowton · 2018-02-02T10:46:18Z

src/java_bytecode/java_bytecode_convert_method.cpp

This thing is rather specific! Probably rename it "add_variable_symbol"?

smowton · 2018-02-02T10:47:33Z

src/java_bytecode/java_bytecode_convert_method.cpp

These aren't very obvious at the callsite -- perhaps use two-valued enums so we don't mix up true, false and false, true?

smowton · 2018-02-02T10:48:44Z

src/java_bytecode/java_bytecode_convert_method.cpp

These don't really need to be members -- they're clearly static helpers

Degiorgio · 2018-02-02T10:55:43Z

@smowton, oks will rebase on top of 1774

Degiorgio · 2018-02-12T10:35:14Z

@smowton , rebase done, can you take a look please?

smowton

Some suggestions

smowton · 2018-02-13T11:21:18Z

src/java_bytecode/java_static_initializers.cpp

INIT_COMPLETE?

instead of 'RETURN'? yes INIT_COMPLETE is better, changing.

@Degiorgio Do not forget to update the documentation above

smowton · 2018-02-13T11:22:47Z

src/java_bytecode/java_static_initializers.cpp

Use _state instead of _s

smowton · 2018-02-13T11:24:47Z

src/java_bytecode/java_static_initializers.cpp

Rename this variable _thread_local rather than just _local to clarify we mean thread-locality not that it's a function local

smowton · 2018-02-13T11:25:22Z

src/java_bytecode/java_static_initializers.cpp

Out of date? AFAIK there is no state named READY anymore

yep this should be RETURN

smowton · 2018-02-13T11:29:50Z

src/java_bytecode/java_static_initializers.cpp

?? Will that work? Presumably we want the other thread to busy-wait for IN_PROGRESS to transition to DONE in this case. If this is indeed magic that symex understands like a wait then write that in the comments.

Yes, that will work. It's exactly how POSIX mutexes are implemented in pthread_mutex_lock, see here:

https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/library/pthread_lib.c#L132

Thanks, we will indeed document it.

cesaro · 2018-02-13T15:45:17Z

src/java_bytecode/java_static_initializers.cpp

Typo: "is used as an optimization"

cesaro · 2018-02-13T19:24:33Z

@smowton all suggestions applied, please have a another look

Degiorgio · 2018-02-15T16:22:23Z

@peterschrammel can you take another look at this please? All the issues you raised should be addressed.

smowton

Sorry, more stuff to fix

smowton · 2018-02-15T16:21:38Z

src/java_bytecode/java_static_initializers.cpp

smowton · 2018-02-15T16:25:46Z

src/java_bytecode/java_static_initializers.cpp

fwiw the value member of a local variable is ignored; it's up to you to generate an initialiser. Therefore recommend passing nil_exprt() there and checking in add-new-symbol that function-scoped (non-global) variables do not attempt to specify an initialiser this way.

smowton · 2018-02-15T16:26:30Z

src/java_bytecode/java_static_initializers.cpp

Non-doxy (//) comment

smowton · 2018-02-15T16:29:08Z

src/java_bytecode/java_static_initializers.cpp

I think this comment is inaccurate, does it belong to the thread-local variable instead? The function-local one is just used to copy the global so you can inspect it and then maybe return outside a critical section.

the comment is misleading agreed. rewording.

We are using a local boolean for inspection on purpose. The reason being that inspecting the global state resulted in symex related propagation issues in multi-threaded code.

smowton · 2018-02-15T16:30:12Z

src/java_bytecode/java_static_initializers.cpp

Also the local should be created in the populate-function-body phase. Only globals should be created at this stage (i.e. the global, the thread-scoped variable, and the function symbol itself).

…itialize

A temporary variable is introduced later for this if_exprt and the mode needs to be known for the variable, other an invariant may fail.

This checks the ID_mode fix for if_expr in preprocessing works correctly.

…yway

This is an implementation detail that need not be exposed to users - the interface is the free function base_type_eq.

... and sort the remaining ones lexicographically.

The previous version of clinit_wrapper did not conform to the JVM specification (section 5.5) as it did not support concurrency. More specifically, the clinit_wrapper has to be carefully synchronised as other threads may try to initialize a given class or interface at the same-time. This commit makes the clinit_wrapper thread-safe by introducing a critical section and two state variables. The commit implements a simplification of the algorithm defined in section 5.5 of the JVM specification. For instance, exceptions thrown during the execution of static initializers are not properly handled.

Setting this option will enable support for analysing multi-threaded java programs. For now, this means that a thread-safe version of clinit_wrapper is generated. This was made opt-in instead of opt-out as the inclusion of thread-safe clinit wrapper has negative implications for performance. Commit also adds appropriate regression tests that use this flag to test the resulting modifications to the clinit_wrapper

Degiorgio requested review from cesaro, mgudemann, peterschrammel, smowton and thk123 as code owners January 31, 2018 16:20

Degiorgio force-pushed the concurrency-support-for-clinit branch from a79f687 to 76b1842 Compare January 31, 2018 16:23

Degiorgio force-pushed the concurrency-support-for-clinit branch from 76b1842 to 9694036 Compare February 1, 2018 10:31

peterschrammel reviewed Feb 1, 2018

View reviewed changes

smowton reviewed Feb 2, 2018

View reviewed changes

Degiorgio force-pushed the concurrency-support-for-clinit branch 2 times, most recently from f8a32ea to 6691b0d Compare February 12, 2018 10:34

Degiorgio force-pushed the concurrency-support-for-clinit branch 4 times, most recently from 7143b9f to 72c061b Compare February 12, 2018 12:55

smowton reviewed Feb 13, 2018

View reviewed changes

cesaro reviewed Feb 13, 2018

View reviewed changes

Degiorgio force-pushed the concurrency-support-for-clinit branch 2 times, most recently from 0b9e580 to bfe8097 Compare February 13, 2018 16:17

Degiorgio force-pushed the concurrency-support-for-clinit branch 3 times, most recently from 43ed109 to 43e69ac Compare February 15, 2018 14:47

smowton reviewed Feb 15, 2018

View reviewed changes

Degiorgio force-pushed the concurrency-support-for-clinit branch 2 times, most recently from de6a0e4 to ef8bf61 Compare February 15, 2018 17:22

tautschnig and others added 22 commits May 2, 2018 17:52

Use iosfwd instead of ostream where possible

c57627c

Use a single global INITIALIZE_FUNCTION macro instead of __CPROVER_in…

60bcdb6

…itialize

Use C++ streams instead of C-style snprintf

dfd6923

Set mode of if_exprt introduced in preprocessing

28cc669

A temporary variable is introduced later for this if_exprt and the mode needs to be known for the variable, other an invariant may fail.

Add test where tmp_if_expr is introduced

a123ca9

This checks the ID_mode fix for if_expr in preprocessing works correctly.

Do not unnecessarily use C string functions

2408c22

Move asserts to invariants (and provide suitable includes)

063d3da

Use pointer_offset_bits instead of locally hacking up what it does an…

87d0dbb

…yway

Move definition of base_type_eqt to .cpp

5b29e22

This is an implementation detail that need not be exposed to users - the interface is the free function base_type_eq.

Remove unused includes

49cfaf7

... and sort the remaining ones lexicographically.

Assign mode to invalid objects

5fcd098

whitespace fix

81331c8

remove do_unwind_module hook

9111c4d

remove unused includes

879e379

remove support for SMT1

cbc4fa2

remove OpenSMT

738cf75

remove bmc_constraints

5c9419a

missing const for parameter

4a8107f

fix a comment

d115904

cleanup the includes in src/java_bytecode

f3d5223

Degiorgio force-pushed the concurrency-support-for-clinit branch from a5ab2ef to 4c7b646 Compare May 2, 2018 16:54

Degiorgio requested review from chrisr-diffblue, forejtv, kroening, martin-cs and romainbrenguier as code owners May 2, 2018 16:54

Degiorgio closed this May 2, 2018

Degiorgio mentioned this pull request May 2, 2018

Making the instrumented clinit_wrapper function thread-safe #2145

Merged

Conversation

Degiorgio commented Jan 31, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

thk123 commented Jan 31, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Degiorgio commented Feb 2, 2018

Uh oh!

Degiorgio commented Feb 12, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Degiorgio Feb 13, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Degiorgio Feb 13, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

cesaro commented Feb 13, 2018

Uh oh!

Degiorgio commented Feb 15, 2018

Uh oh!

smowton left a comment

Degiorgio commented Jan 31, 2018 •

edited

Loading

Degiorgio commented Feb 12, 2018 •

edited

Loading

Degiorgio Feb 13, 2018 •

edited

Loading

Degiorgio Feb 13, 2018 •

edited

Loading

Degiorgio Feb 15, 2018 •

edited

Loading