Debugging a Java multi-threaded program

We consider the Java program described in https://www.cs.unh.edu/~charpov/programming-tlabuffer.html. This Java program consists in several threads that communicate using a single shared buffer (class Buffer). Some of the threads are producers that write to the shared buffer. The other threads are consumers that read data from the shared buffer.

As explained in the document at the link above, this program has a bug: the system may deadlock. This was detected on a production version of the application. The author has been able to reproduce the bug through testing. However, it required to let the system run for a very long time before the bug occured. This is unsatisfactory as this mostly relies on luck. Moreover, the resulting trace is so long that debugging from the trace is almost unachievable.

A starter

The author has modeled the system in TLA+ and used the TLC model-checker to detect the bug and get a short trace leading to the deadlock. Our goal is to reproduce his methodology in a slightly different settings:

  • we will model the Java program in the higher-level language PlusCal instead of directly in TLA+ (although some definitions in TLA+ will be useful)
  • we also claim that the model can be improved

Read the document at the link above. You need to fully understand the Java code (refering to the language specification), his TLA+ model, the issue that is identified by the author, and his solution. In particular, you should answer the following questions:

  1. Which standard data structure is implemented by the Java class Buffer?
  2. Why are some methods synchronized and what does it imply on the runs of the program?
  3. How do wait(), notify() and notifyAll() work?
  4. What are the CONSTANTS in the TLA+ model, and what is the goal of the ASSUME condition and the TypeInv definition set by the author?
  5. What is modeled by buffer and waitSet, and how are they modeled?
  6. From the Java documentation, argue why the definitions of Notify, NotifyAll and Wait model accurately the semantics of the corresponding Java methods.
  7. Justify why the definitions Put and Get correspond to the semantics of the Java methods.
  8. Why do the Init, Next and Prog definitions capture exactly the runs of the Java program? Justify
  9. Finally, explain why model-checking the property NoDeadlock corresponds to searching for the bug in the author’s TLA+ model.

Modeling the buggy Java program in PlusCal

Our ultimate goal is to provide a PlusCal model that improves the TLA+ model of the author. We start from the skeleton file java_prodcons_skel.tla that builds on the ideas of the author. The goal is to model the Java code containing the bug in such a way that (1) the model behaves similary to the Java program and (2) the bug can be detected from the model using the TLC model-checker.

Modeling the data structures

A first step consists in identifying the data structures in the Java code that need to ne modeled in PlusCal.

  1. What are the data structures used by this Java code?
  2. The Java code of the Buffer class has two methods put() and get() that do two things. First, they check if writing or reading from the buffer can be performed. Then, they update the buffer. We suggest to split these two parts, and write macros or definitions for the methods isEmpty, isFull, next, push and pop (or the subset that you have identified as necessary). The macros push and pop perform the modifications on the buffer.
  3. Proceed similarly for the other data structures that you have identified.

Implementing the processes

Now, we can model the processes.

  1. Write a PlusCal algorithm of the producer processes. It should model the behaviors of the Java put() method.
  2. Similarly, the algorithm of a consummer should have the same behaviors as the Java method get().
  3. How can we detect the bug using the TLC model-checker on your model? Check that your model exhibits a similar error than the author’s TLA model for the settings described in the paper (3 producers, 2 consumers and a buffer of capacity 2).
  4. Replace the calls to notify() by notifyAll() in your model. Check that the bug disapperas and explain why.

Fixing the PlusCal model

Using your model, you have been able to identifiy the bug that was mentionned by the author. Our goal now is to fix the model, in such a way that we can prove it behaves correctly. In this part, we consider an instance of the system with 3 producers, 2 consumers and a buffer of capacity 2. Copy your buggy model in a new .tla file that you will be working on from now.

  1. Identify a way to fix your model, that can be implemented in Java.
  2. Modify your PlusCal model accordingly. Then, check that your model does not exhibit the error anymore.
  3. One you have checked that your model is correct, implement your solution in the Java code.

Improving the model

In the previous section, you have been able to fix your model, and check that your new model is correct for 3 producers, 2 consumers and a buffer of capacity 2. Our goal is to be able to model-check bigger instances of the system.

  1. Check that your solution is correct for an instance with 12 producers, 10 consumers and a buffer of capacity 10. Interrupt model-checking if it has not terminated within 2 minutes.
  2. If verification takes more than 2 minutes, your model is uselessly complex. Identify the issue from the section “Limitations of Model Checking” in the document.
  3. The issues in your model can come from different parts: too many interleavings of processes which do not correspond to actual runs of the Java program, data structures that could be modeled in a more abstract way, etc. Identify parts of your model taht can be improved. Find solutions and argue that they are correct. Update your model until you manage to verify the bigger instance within 2 minutes.
  4. What can you conclude on your model, and on the Java program?