xekoukou / tla-agda-v2

GNU Affero General Public License v3.0
0 stars 0 forks source link

Runtime Strongly Fairness. #1

Open xekoukou opened 6 years ago

xekoukou commented 6 years ago

The scheduler of actions needs to pick actions that have not performed any actions recently, so as to have the property of strong fairness for all actions, even if our specification does not require it.

One way to do it is to log the number of invocations of an action and pick the one with the lower number for execution.

xekoukou commented 6 years ago

Care needs to be taken when actions are parametric to a variable and fairness depends on that variable.

ex. Performing a specific action for a specific client constantly will not allow the execution of the same action for other clients. Here fairness takes into account the parameter client.

xekoukou commented 5 years ago

page 23 theorem 2.7 https://members.loria.fr/SMerz/talks/argentina2005/slides.pdf