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