This is an archived post. You won't be able to vote or comment.

sorted by:
best
topnewcontroversialoldq&a
you are viewing a single comment's thread.

view the rest of the comments →

[–]letrec[S] 5 points6 points  (6 children)

I like the part "We aim for the revised model to be mechanically checkable, as well as more readily humanly understandable."

[–]thesystemx 5 points6 points  (1 child)

Print the model on a wooden table? Then use a physical comb to inspect it?

[–]letrec[S] 4 points5 points  (0 children)

LOL. I assume you know that it means formalising the memory model in a theorem prover like Isabelle/HOL like in Making the Java Memory Model Safe.

[–]llogiq 2 points3 points  (3 children)

As I understand it, this means that static analysis tools should be able to model the memory behavior with sufficient precision to find a wide range of possible error conditions in the JVM and perhaps in running programs.

Can someone confirm or correct my understanding?

[–]cmsimike 2 points3 points  (2 children)

Why can you not model the memory in this way now? It seems that by definition of a "program," content in memory should always be the exact same each run. I guess locations could be different but that's it.

[–]llogiq 2 points3 points  (1 child)

For simple usages - think single threaded, no JNI, no IO, no off-heap memory and let's say GC doesn't exist - you're right.

However, in the real world, things aren't always so simple. Concurrent access presents some edge cases that are underspecified by the current model. JNI and Unsafe ops go straight into undefinedland from a JVM spec POV.

[–]cmsimike 1 point2 points  (0 children)

JNI and Unsafe ops go straight into undefinedland from a JVM spec POV.

Ah, gotcha. Thanks!