On Wed, Nov 2, 2022 at 5:35 PM Robert Engels <reng...@ix.netcom.com> wrote:
> I think this can be disproven. > > Given a function A with a reentrant lock, it can be rewritten as A with > non-reentrant lock and A’ without a lock where A’ is the original A function > body. > > A’ would then be susceptible to the original “reasoning difficulties” without > any locking. I think it shows that any complex function, especially those > with recursion, have the same difficulties. I think up to this point the reasoning is correct - even though it IMO demonstrates the opposite: If A' handles the invariants incorrectly then a reentrant lock guarding the A will not help to fix the problem. IOW, not using a reentrant lock is better because a deadlock/crash is safer than corrupting data/state. > Due to sequential consistency, A’ must be correct, since a non-reentrant lock > forces a single thread of execution - making A’ and A equivalent. I think this holds differently: Iff A' is correct then A' and A are equivalent [in the first approximation ignoring the locking]. So again, in all cases where the correctness of A' cannot be proven, avoid "fixing" it by a reentrant lock. -- You received this message because you are subscribed to the Google Groups "golang-nuts" group. To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/golang-nuts/CAA40n-UG%3DpNx7Xkt5UHduS5F5DtiCE1gcK3fL7t-HMjWDtAK1w%40mail.gmail.com.
