v19 (Traces): Print (partial) implementation executions.

README.md

@@ -13,6 +13,47 @@ This tutorial is work in progress. More chapters will be added in the future. In
 
 --------------------------------------------------------------------------
 
+### v19 (Traces): Print (partial) implementation executions.
+
+Having finished the proof of the deadlock fix below, we shift our attention to the (Java) implementation that we assume can still deadlock.  However, before we apply the fix of two mutexes, we use TLC to check if the implementation allows executions that violate the ```BlockingQueue``` spec.  In other words, we check if the implementation correctly implements the TLA+ spec (which we know it does not).  To do so, we print an execution to stdout with the help of the low-overhead [Java Flight Recorder](https://en.wikipedia.org/wiki/JDK_Flight_Recorder) that we can consider a very powerful logging framework.  However, plain logging to stdout - with a high-precision timestamp - would have worked too.   To activate JFR, run the app with:
+
+```bash
+java -XX:StartFlightRecording=disk=true,dumponexit=true,filename=app-$(date +%s).jfr -cp impl/src/ org.kuppe.App
+
+# Kill the process after a few seconds.
+
+# app-1580000457.jfr is the flight recording created by the previous command.
+java -cp impl/src/ org.kuppe.App2TLA app-1580000457.jfr 
+[ op |-> "w", waiter |-> "c" ],
+[ op |-> "e" ],
+[ op |-> "e" ],
+[ op |-> "d" ],
+[ op |-> "e" ],
+[ op |-> "d" ],
+[ op |-> "d" ],
+[ op |-> "e" ],
+[ op |-> "e" ],
+[ op |-> "d" ],
+[ op |-> "d" ],
+[ op |-> "e" ],
+[ op |-> "e" ],
+[ op |-> "e" ],
+[ op |-> "d" ],
+[ op |-> "d" ],
+[ op |-> "e" ],
+[ op |-> "e" ],
+[ op |-> "w", waiter |-> "p" ],
+[ op |-> "d" ],
+[ op |-> "e" ],
+
+```
+
+It is important to observe that the log statements only log the operation (deq|enq|wait) and the thread that calls wait. The log does not contain the size or content of the buffer, the thread that gets notified, or the thread that executes.
+
+(JFR requires Java 11 or newer).
+
+--------------------------------------------------------------------------
+
 ### v18 (TLAPS): Co-domain of buffer not relevant for proof.
 
 No need to say anything about the co-domain of buffer in the proof.  What is enqueued

impl/src/org/kuppe/App2TLA.java

@@ -0,0 +1,74 @@
+package org.kuppe;
+
+import java.io.IOException;
+import java.nio.file.Paths;
+import java.util.Comparator;
+import java.util.List;
+
+import jdk.jfr.Category;
+import jdk.jfr.Label;
+import jdk.jfr.Name;
+import jdk.jfr.StackTrace;
+import jdk.jfr.consumer.RecordedEvent;
+import jdk.jfr.consumer.RecordingFile;
+
+public class App2TLA {
+
+	@Label("Buffer Deq Operation")
+	@Name("app.bufDeqOp")
+	@Category("MyApp")
+	@StackTrace(false)
+	static class BufferDeqEvent extends jdk.jfr.Event {
+	}
+
+	@Label("Buffer Deq Operation")
+	@Name("app.bufEnqOp")
+	@Category("MyApp")
+	@StackTrace(false)
+	static class BufferEnqEvent extends jdk.jfr.Event {
+	}
+
+	@Label("Buffer Wait Operation")
+	@Name("app.bufWaitOp")
+	@Category("MyApp")
+	@StackTrace(false)
+	static class BufferWaitEvent extends jdk.jfr.Event {
+
+		@Label("(p)roducer or (c)onsumer")
+		String type;
+
+		public BufferWaitEvent(String type) {
+			this.type = type;
+		}
+	}
+
+	public static void main(final String[] args) throws IOException {
+		final List<RecordedEvent> recordedEvents = RecordingFile
+				.readAllEvents(Paths.get(args.length > 0 ? args[0] : "app.jfr"));
+
+		// Order events chronologically based on the system's clock (that hopefully has
+		// sufficient precision).
+		// TODO: Logical clock instead of real/global clock.
+		recordedEvents.sort(new Comparator<RecordedEvent>() {
+			@Override
+			public int compare(RecordedEvent o1, RecordedEvent o2) {
+				return o1.getStartTime().compareTo(o2.getStartTime());
+			}
+		});
+
+		printTrace(recordedEvents);
+	}
+
+	private static void printTrace(final List<RecordedEvent> events) {
+		// Format each step in the execution as a TLA+ record.
+		for (RecordedEvent event : events) {
+			if (event.getEventType().getName().equals("app.bufDeqOp")) {
+				System.out.printf("[ op |-> \"d\" ],\n");
+			} else if (event.getEventType().getName().equals("app.bufEnqOp")) {
+				System.out.printf("[ op |-> \"e\" ],\n");
+			} else if (event.getEventType().getName().equals("app.bufWaitOp")) {
+				System.out.printf("[ op |-> \"w\", waiter |-> \"%s\" ],\n", event.getString("type"));
+			}
+		}
+	}
+}

impl/src/org/kuppe/BlockingQueue.java

@@ -1,5 +1,9 @@
 package org.kuppe;
 
+import org.kuppe.App2TLA.BufferDeqEvent;
+import org.kuppe.App2TLA.BufferEnqEvent;
+import org.kuppe.App2TLA.BufferWaitEvent;
+
 public final class BlockingQueue<E> {
 
 	private final E[] store;
@@ -21,13 +25,15 @@ public BlockingQueue(final int capacity) {
 	 */
 	public synchronized void put(final E e) throws InterruptedException {
 		while (isFull()) {
+			new BufferWaitEvent("p").commit();
 			System.out.println("Buffer full; P waits");
 			wait();
 			System.out.println("P notified");
 		}
 		notify();
 
 		// Add e and do bookkeeping.
+		new BufferEnqEvent().commit();
 		append(e);
 	}
 
@@ -39,13 +45,15 @@ public synchronized void put(final E e) throws InterruptedException {
 	 */
 	public synchronized E take() throws InterruptedException {
 		while (isEmpty()) {
+			new BufferWaitEvent("c").commit();
 			System.out.println("Buffer empty; C waits");
 			wait();
 			System.out.println("C notified");
 		}
 		notify();
 
 		// Remove e and do bookkeeping.
+		new BufferDeqEvent().commit();
 		return head();
 	}