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.
Due to sequential consistency, A’ must be correct, since a non-reentrant lock
forces a single thread of execution - making A’ and A equivalent.
Trivial functions are easy to reason about no matter the locking strategy.
> On Nov 2, 2022, at 7:49 AM, Eli Lindsey <e...@siliconsprawl.com> wrote:
> Reentrant locks make any given critical section harder to understand because
> you must also understand the calling pattern that led there to know which
> invariants have been upheld and which may have been violated due to a
> still-in-progress critical section higher up the call chain.
>
> For example, Average.Value() in the example is making the assumption that sum
> and count have been appropriately updated in lockstep. But if the lock is
> reentrant, this may not be true. Average is small enough that it’s trivial to
> check if this is a problem (ie. that Value is not called from Add while
> sum/count mismatch); more complex code is not, especially when it encounters
> future maintainers.
>
> -eli
>
>> On Nov 2, 2022, at 7:43 AM, Robert Engels <reng...@ix.netcom.com> wrote:
>>
>> I am curious though for an example that shows how a reentrant lock could
>> violate this?
>>
>>> On Nov 2, 2022, at 2:38 AM, peterGo <go.peter...@gmail.com> wrote:
>>>
>>> Guanyun,
>>>
>>> I tried to think of a simple example.
>>>
>>> type Average struct {
>>> sum float64
>>> count int64
>>> mx sync.Mutex
>>> }
>>>
>>> https://go.dev/play/p/4SLCLuqG246
>>>
>>> 1. An invariant represents a condition that does not change while the
>>> process progresses - Niklaus Wirth.
>>>
>>> 2. The additional invariant--Average = sum / count--is specific to the data
>>> structure that the mutex mx guards.
>>>
>>> 3. The shared variables sum and count are part of an invariant.
>>>
>>> 4. The Add method temporarily violates the invariant by updating sum but
>>> restores the invariant by updating count.
>>>
>>> Peter
>>>
>>> On Wednesday, November 2, 2022 at 12:49:41 AM UTC-4 name....@gmail.com
>>> wrote:
>>>> Hello,
>>>>
>>>> This is a passage in book <The Go Programming Language>:
>>>> --------------------------------------------------------------------------------------------------------
>>>> There is a good reason Go’s mutexes are not re-entrant.
>>>>
>>>> The purpose of a mutex is to ensure that certain invariants of the shared
>>>> variables are
>>>> maintained at critical points during program execution.
>>>>
>>>> One of the invariants is "no goroutine is accessing the shared variables",
>>>> but there may be additional invariants specific to the data structures
>>>> that the mutex guards.
>>>>
>>>> When a goroutine acquires a mutex lock, it may assume that the invariants
>>>> hold. While it holds the lock, it may update the shared variables so that
>>>> the invariants are temporarily violated.
>>>>
>>>> However, when it releases the lock, it must guarantee that order has been
>>>> restored
>>>> and the invariants hold once again.
>>>>
>>>> Although a re-entrant mutex would ensure that no other goroutines are
>>>> accessing the shared variables, it cannot protect the additional
>>>> invariants of those variables.
>>>>
>>>> --------------------------------------------------------------------------------------------------------
>>>>
>>>> This passage is difficult for me to understand:
>>>> 1. How to understand invariants "invariants"?
>>>> 2. What kind of scenarios does “additional invariants” refer to?
>>>> 3. What is the relationship between "shared variables" and "invariants"?
>>>> 4. What does "...guarantee that order has been restored..." mean?
>>>>
>>>> Thanks,
>>>> Guanyun
>>>
>>>
>>> --
>>> 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/c2b53c11-4552-4b9a-a528-fc179ba0f513n%40googlegroups.com.
>>
>>
>> --
>> 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/6F217FB7-077E-4CBE-B46E-4ADB7D7461A3%40ix.netcom.com.
>
> --
> 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/9875F919-83A9-43E4-88EC-81D6C447ED9A%40siliconsprawl.com.
--
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/C7DDECB5-207B-4B01-937D-D86BD6BD6AD0%40ix.netcom.com.
