Making the instrumented clinit_wrapper function thread-safe #1786

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

+/// This wrapper is called immediately before any read or write of a static
+/// field or whenever an instance of the class is created.
+/// When class \p classname does not need static initialization we
+/// return a nil irep.  We also explicitely avoid introducing calls to the


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

src/java_bytecode/java_bytecode_convert_method.cpp

+
+  // Initialize the syper-class C' and
+  // the implemented interfaces l_1 ... l_n.
+  // see JVM Spec p.359 step 7, for the exact defination of


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

src/java_bytecode/java_bytecode_convert_method.cpp

+  const clinit_statest state)
+{
+  mp_integer initv(static_cast<int>(state));
+  constant_exprt init_s=from_integer(initv, java_int_type());


Do you require a full int here?

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

src/java_bytecode/java_bytecode_convert_method.cpp

-/// place, calls the actual <clinit> method if not, and initializes super-
-/// classes and interfaces.
-/// \param classname: Class name
+/// This function retrieves from or creates into the symbol table a wrapper


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

+  // if we are initializing class C due to a use of class C within method
+  // `C.<clinit>` then avoid the recursive (and unnecessary) call to
+  // the wrapper.
+  const irep_idt &real_clinit_name=id2string(classname)+".<clinit>:()V";


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

+    true, false);
+
+  code_blockt function_body;
+  codet atomic_begin(ID_atomic_begin);


Consider making a std_code entry for these?

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

src/java_bytecode/java_bytecode_convert_method.cpp

+    function_body.add(conditional);
+  }
+
+  // Initialize the syper-class C' and


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

src/java_bytecode/java_bytecode_convert_method.cpp

+  // This is achieved  by iterating through the base types and
+  // adding recursive calls to the clinit_wrapper()
+  {
+    const symbolt &class_symbol=*symbol_table.lookup(classname);


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

src/java_bytecode/java_bytecode_convert_method.cpp

+  const irep_idt &name,
+  const typet &type,
+  const exprt &value,
+  const bool is_thread_local,


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

+/// /param is_thread_local: if true this symbol will be set as thread local
+/// /param is_static_lifetime: if true this symbol will be set as static
+/// /return returns new symbol.
+symbolt java_bytecode_convert_methodt::add_new_symbol(


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

+  const irep_idt &name,
+  const typet &type,
+  const exprt &value,
+  const bool is_thread_local,


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

+///   equal exprt.
+/// /return returns a equal_exprt, equating \p symbol_expr to the integer
+///   representation of \p state
+equal_exprt java_bytecode_convert_methodt::gen_clinit_eqexpr(


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

+{
+  NOT_INIT,
+  IN_PROGRESS,
+  RETURN


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

-  equal_exprt check_already_run(
-    already_run_symbol.symbol_expr(),
-    false_exprt());
+  const symbolt &clinit_s_sym =


Use _state instead of _s

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

src/java_bytecode/java_static_initializers.cpp

+
+  add_new_symbol(
+    symbol_table,
+    clinit_local_state_variable_name(class_name),


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

+///     java::C::__CPROVER_clinit_state = IN_PROGRESS
+///     was_ready = false;
+///   }
+///   else If(java::C::__CPROVER_clinit_state == READY)


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

+///   java::C::__CPROVER_clinit_local_state = RETURN;
+///
+///   ATOMIC_BEGIN
+///   Assume(java::C::__CPROVER_clinit_state != IN_PROGRESS)


?? 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

+    true);
+
+  // Create a local variable "was_ready". This variable is used optimization as
+  // an optimization to make even more clear to the symex engine that it does


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

+///   equal exprt.
+/// /return returns a equal_exprt, equating \p symbol_expr to the integer
+///   representation of \p state
+equal_exprt


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

src/java_bytecode/java_static_initializers.cpp

+    symbol_table,
+    clinit_local_init_complete_var_name(class_name),
+    bool_typet(),
+    false_exprt(),


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

+  static_assert((int) clinit_statest::INIT_COMPLETE==2, "Check comment above");
+#endif
+
+  /// bool init_complete;


Non-doxy (//) comment

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

src/java_bytecode/java_static_initializers.cpp

+    true,
+    true);
+
+  // Create a local variable "init_complete". This variable is used as an


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

+  // Create a local variable "init_complete". This variable is used as an
+  // optimization to make even more clear to the symex engine that it does not
+  // need to unwind ifinitely many copes of the wrapper
+  add_new_symbol(


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

Making the instrumented clinit_wrapper function thread-safe #1786

Making the instrumented clinit_wrapper function thread-safe #1786

Conversation

Degiorgio commented Jan 31, 2018 • edited Loading

thk123 commented Jan 31, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio commented Feb 2, 2018

Degiorgio commented Feb 12, 2018 • edited Loading

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio Feb 13, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio Feb 13, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cesaro commented Feb 13, 2018

Degiorgio commented Feb 15, 2018

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Degiorgio Feb 15, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this 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