Before any proof, the debate would benefit from more precise definitions. For instance, the issue around the usage of fencing tokens to reject any late usage o

Before any proof, the debate would benefit from more precise definitions. For instance, the issue around the usage of fencing tokens to reject any late usage of a lock is unclear just because the protected resource and its access are themselves unspecified. Is the resource distributed or not? If distributed, does the resource has a mean to ensure that tokens are increasing over all the nodes? Does the resource have a mean to rollback any effects done by a client which session is interrupted by a timeout? Likewise for the timing arguments. It seems clear to everyone that timeouts provide only some protection rather than a guarantee. A more precise timeline of the worst case scenario will help to estimate that protection given the misc timeout values and clock shifts.