[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


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.



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.