I just managed to make my first sync point recording on the MacBook. I had to remove the instrumentation strategy that assigns object IDs and remove the calls to get those IDs in the strategy for synchronized blocks.
The problem could be in either the place that assigns the object ID, the place that queries it, or perhaps also just in one special class. For Windows, I’ve also had to exclude a few classes, so that might be the case for the Mac too.
I also talked to Cormac Flanagan again today. He had sent me a paper draft yesterday that outlined a technique similar to our instrumentation for model checking. The draft, unfortunately, didn’t answer my questions. He said, though, that he had also used a flag to prevent internal logic from changing the behavior of the program. Another alternative was to use two copies of Java runtime classes, one copy that is instrumented and used by the user program, and one that isn’t for the recording software.
It seems like the problem is either adding the overridden
$$$getObjectId$$$ method or the
$$$objectId$$$ field to one or several classes that are somehow “touchy” in Apple’s VM, because adding the default method to
java.lang.Object and calling it at the sync points works.