Hi Nikita,
I started to implement the algorithms as described in your recorded talks. In your skeleton code, the modelCheckingTest for the FCQueue expects obstruction-freedom. The flat combining algorithm requires a lock to be able to enter the combine-and-apply step. Therefore, obstruction-freedom can't be guaranteed. Or I'm wrong?
This is my implementation of the FCQueue which only successfully executes the modelCheckingTest if I exclude checkObstructionFreedom(): https://github.com/rendner/Hydra2022/blob/master/src/fcqueue/FCQueue.kt
Hi Nikita,
I started to implement the algorithms as described in your recorded talks. In your skeleton code, the
modelCheckingTestfor theFCQueueexpects obstruction-freedom. The flat combining algorithm requires a lock to be able to enter the combine-and-apply step. Therefore, obstruction-freedom can't be guaranteed. Or I'm wrong?This is my implementation of the
FCQueuewhich only successfully executes themodelCheckingTestif I excludecheckObstructionFreedom(): https://github.com/rendner/Hydra2022/blob/master/src/fcqueue/FCQueue.kt