Re: [tlaplus] What does it mean to specify liveness for a "sys implementation"?

Hello,

any TLA+ specification describes the evolution of a universe that contains the system we are interested in. Its basic form

Init /\ [][Next]_vars

allows for infinite stuttering on "vars": although the universe doesn't stop, it may be too busy for making our little system advance. This is true independently of the level of abstraction at which the specification is written. If you are only interested in evolutions of the universe in which certain (enabled) actions of the system do occur, you need to use fairness conditions to specify which actions should occur, and of course these fairness conditions should reflect the environment in which the system is run.

At a more down-to-earth level, your question actually contains the answer:

For example, even though we specify SF(RdMiss(p)), whether it's guaranteed or not depends
on the hardware scheduling and it's possible the memory hardware system is unfair to one of processors.

If the support of your write-through cache may be unfair to a processor, you should probably not assert the fairness condition. Or only assert it as a formal exercise to ensure that such potential unfairness is the only reason why your liveness property could be violated.

Stephan

On 2 May 2019, at 06:59, Oliver Yang <olilent2ctw@xxxxxxxxx> wrote:

Hi ALL,

As stated in the subject, I am a bit confused about the meaning of specifying liveness properties for a "sys implementation".

I will use Linearizable Memory example from "Specifying Systems" book as an example to illustrate my confusion.

It makes perfect sense to specify liveness properties for a "sys specification" since "sys specification" is suppose to describe
what the system should do. For example, we want to specify that every request receive a response in the specification of linearizable memory.

However, why do we want to specify liveness in write-through cache implementation in terms of WF/SF of subactions?
Isn't that "sys implementation" is suppose to describe how instead of what? And weak fairness/strong fairness should
be considered as what. For example, even though we specify SF(RdMiss(p)), whether it's guaranteed or not depends
on the hardware scheduling and it's possible the memory hardware system is unfair to one of processors.

Thanks,

Oliver

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.