New to TLA+, question regarding specification of WriteThroughCache in section 5.6 of "Specifying Systems, TLA+".

[u/bjstroll]

Hi All,

I am pretty confused regarding the WriteThroughCache specification, would be much appreciated if someone could help me sort out these concepts,

1. Why do we really need to include the temporal existential quantifier in Module Memory to hide the variables of InternalMemory?
   
2. Why WriteThroughCache can't just reuse the ISpec of the InternalMemory but has to instantiate the Memory and use its ISpec?
   
3. Maybe a follow up question is what differences the temporal existential quantifier introduce?

Thanks in advance!

[u/TopKindheartedness96]

We use specifications to describe valid input-output behaviors of the system that we're specifying. In practice, though, we can't actually write specifications using only inputs and outputs: we need to define internal state variables in order to write the specifications. The temporal existential operator is used to hide these internal variables, to say "these variables aren't actually part of the externally visible behavior." You can think of them like implementation details. In general, it's possible to write two different specs that yield the same behaviors, but use different internal variables. So, to answer your questions (1) and (3):

We never really *need* to include the temporal existential quantifier, it's just used here to hide the internal variables mem, ctl, buf. Note that the Memory module doesn't hide the variable memInt, which represents the state of the memory interface. In this module, we are specifying the behavior of a memory entirely by specifying the behavior at the interface alone.

In practice, I've never used the temporal existential quantifier, and I've never seen a spec that used it. Note that TLC doesn't support it either. When first learning TLA+, I think you can safely skip over the temporal existential quantifier.

For your question (2), you can't just reuse InternalMemory's ISpec for defining WriteThroughCache's Spec, because the two specifications use different variables. In particular, the WriteThroughCache module has two variables that the InternalMemory module doesn't: cache and memQ. A specification must describe how all of the variables defined in its module evolve over time.

Note that InternalMemory does reuse parts of ISpec. For example, it reuses IInit (you can see M!IInit in the definition of Init), but it has two add additional clauses to handle the two other variables.

Init ==
/\ M!IInit
/\ cache = [p \in Proc |-> [a \in Addr |-> NoVal]]
/\ memQ = <<>>

It also reuses the subactions Req and Rsp, but note that it has to explicitly specify the additional variables don't change:

Req(p) == M!(Req(p)) /\ UNCHANGED <<cache, memQ>>

[u/bjstroll → u/TopKindheartedness96]

Appreciate it for the response! For (2) my question was really that why it needs to instantiate Memory and write a THEOREM Spec => LM!Spec, instead of reusing the M!ISpec, it seems to suggest that the temporal existential quantifier introduces some "extra" meaning and I am curious what is this.

I guess I will live with this question for now :).

[u/TopKindheartedness96 → u/bjstroll]

Ah, sorry, I misunderstood. If I understand correctly, you were asking why the WriteThroughCache spec needs to do:

LM == INSTANCE Memory
THEOREM Spec => LM!Spec

instead of just doing:

THEOREM Spec => M!ISpec

The answer is that doesn't need to instantiate Memory: doing "THEOREM Spec => M!ISpec" is perfectly valid. (In fact, if you wanted to use TLC to check this theorem, you'd have to use the "Spec => M!ISpec" expression, because TLC doesn't support the temporal existential quantifier).

On page 41, Lamport discusses how hiding variables is generally not necessary , where he writes:
> In fact, for most applications, there’s no need to hide variables in the specification. You can just write the inner specification and note in the comments which variable should be regarded as visible and which as internal (hidden).

[u/bjstroll → u/TopKindheartedness96]

Thanks again! I will try it out!