TLA+ | The way to specify

Hi all!

I am trying to check the conformity of concurrent Java programs to TLA+ specifications by "running" them in a TLA+ formalization of the JVM specification. In this context I wrote two TLA+ formulas: The first one describes the execution of a single Thread in the JVM, while the second one composes multiple threads and would ideally allow them to move at the same time, if monitors etc allow. It is somehow comparable to the ClockArray example in Mr. Lamport's "Specifying Systems", page 139, just that there are also constraints on the combination of thread states, as if it was (for example) forbidden that multiple clocks show the same time in one global state. Additionally the number of threads that the JVM manages is variable.

While the single threads "run" fine in TLC I am troubled to find a good way to express the composition, that TLC accepts. Here is a simplified example of the formulas I would like to get TLC compatible. To make it readable I reduced the complexity of the thread module to a simple program counter and left away the global constraints, which I think I would be able to handle.

---- MODULE Thread ----
VARIABLE pc
LOCAL INSTANCE Integers
----
Init == pc = 0
Next == pc' = pc+1
====

---- MODULE TLAJVM ----
VARIABLE pcs
Thread(i) == INSTANCE Thread WITH pc <- pcs[i]
----
Init ==
    (* start with one Thread *)
    /\    DOMAIN(pcs) = {1}

    (* Thread!Init has to be true for all threads *)
    /\    \forall i \in DOMAIN(pcs): Thread(i)!Init

Next ==
    (* after a regular "Next" step the amount of threads is still the same *)
    /\    DOMAIN(pcs') = DOMAIN(pcs)

    (* all threads step *)
    /\    \forall i \in DOMAIN(pcs): Thread(i)!Next
====

Is there a way to formalize this in a way that TLC takes it? The ClockArray example uses the "IsFcnOn" formula defined on page 140 to describe the global state. However, while humans can compute possible next states out of a given state, the IsFcnOn invariable and the action formulas for each single clock just fine, TLC needs pcs' to be defined as either "pcs' = ..." or "pcs' \in ..." as far as I understand. Does anybody have an idea how to rewrite the above formula to this form?

I first thought that the TLA+ translations of multiprocess PlusCal algorithms might yield an example, but after reading the "Next" formula on page 63 of "A PlusCal User's Manual" it seems to me that in PlusCal only one processes is allowed to advance per Next step.

For now I have resigned myself to use two alternating actions in the TLAJVM. One that chooses non-deterministically which thread gets run next and a second one that advances that thread while all other threads hold still. However, this introduces interleaving where I would prefer true concurrency and has bad effects on the number of states and the complexity of the mappings I draw from the TLAJVM into the original TLA+ specifications of the programs. Here is a (simplified) version of my current solution:

---- MODULE TLAJVM ----
VARIABLE pcs

VARIABLE threadMovingI
VARIABLE pc
VARIABLE move
----
Thread == INSTANCE Thread WITH pc <- pc (* just to be explicit here *)

Init ==
	/\	Thread!Init (* this determines pc *)
	/\	pcs = << pc >>
	/\	threadMovingI = FALSE
	/\	move = FALSE

Prepare ==
	/\	move = FALSE

	/\	UNCHANGED pcs
	/\	threadMovingI' \in DOMAIN(pcs)
	/\	pc' = pcs[threadMovingI']
	/\	move' = TRUE

Move ==
	/\	move = TRUE

	/\	Thread!Next (* this determines pc' *)
	/\	pcs' = [pcs EXCEPT ![threadMovingI] = pc]
	/\	threadMovingI' = FALSE
	/\	move' = FALSE

Next == Prepare \/ Move

TLAJVM == Init /\ [][Next]_<<pcs,threadMovingI,pc,move>>
====

I would be glad if anyone can give me hint how to express true concurrency of the thread movements in a way that TLC can compute the next states and check my refinement mappings.

Thanks a lot for reading this far and any thoughts on it you might share ;)

TLC was not designed to handle the kind of synchronous process composition that you want. (I find the term "true concurrency" both pretentious and misleading, since the formalism(s?) that go by that name are not conducive to describing physical concurrency.) I have never found such synchronous composition to be a natural way to represent the class of problems that I have observed in practice, so I have not been interested in tools for checking such specifications. (However, the TLAPS proof system should have no problem with them.)

It appears to be impossible to write a philosophically correct spec of the form you want that can be checked by TLC. On the other hand, if your purpose is to try to find and eliminate bugs in the specification, then I suggest that you write a spec with a fixed number of threads that TLC can check. In your example, this can be done by something like

VARIABLES pc1, pc2, pc3
Thread1 == INSTANCE Thread with pc <- pc1
Thread2 == INSTANCE Thread with pc <- pc2
Thread3 == INSTANCE Thread with pc <- pc3
Init == Thread1.Init /\ Thread2.Init /\ Thread3.Init
Next == Thread1.Next /\ Thread2.Next /\ Thread3.Next
...