Contracts for protected objects: internal call cannot appear in precondition of protected operation

Contracts for protected objects: internal call cannot appear in precondition of protected operation

[reinert]

Hello,

I tried to use pre-conditions for an entry in a protected object.
Say (in the specification):

   entry E1 with Pre => test1;   

This seems OK when test1 is external (defined outside the protected object).

However, when test1 is defined inside the protected object, I get:

internal call cannot appear in precondition of protected operation

(I assume this is related to avoid deadlock - but testing from outside
here should not give deadlock?)

I also would like to include (for security) a test on a variable
defined in the private part of the protected object). Anyhow possible?
I do not mange to include pre/post conditions in the body of my
protected object. I missed something?

reinert

Re: Contracts for protected objects: internal call cannot appear in precondition of protected operation

[Randy Brukardt]

That's not allowed, as it would require extra mutual exclusion. Since that 
exclusion would have to be separate from the protected action (necessary 
since the entry may not be open when the call is made), you'd also have a 
race condition (the precondition could be evaluated with one value, the 
value then changed, and then later the entry accepted). Best practices is 
always that preconditions should only depend on the parameters to a call 
(regardless of the kind of call involved).

                        Randy.


"reinert" <reinkor@gmail.com> wrote in message 
news:4ed8fa1e-0b4d-4d6b-bc36-0236f6965db0@googlegroups.com...
> Hello,
>
> I tried to use pre-conditions for an entry in a protected object.
> Say (in the specification):
>
>   entry E1 with Pre => test1;
>
> This seems OK when test1 is external (defined outside the protected 
> object).
>
> However, when test1 is defined inside the protected object, I get:
>
> internal call cannot appear in precondition of protected operation
>
> (I assume this is related to avoid deadlock - but testing from outside
> here should not give deadlock?)
>
> I also would like to include (for security) a test on a variable
> defined in the private part of the protected object). Anyhow possible?
> I do not mange to include pre/post conditions in the body of my
> protected object. I missed something?
>
> reinert 

Re: Contracts for protected objects: internal call cannot appear in precondition of protected operation

[reinert]

Thanks, Got it :-)

reinert

fredag 29. mai 2020 04.11.49 UTC+2 skrev Randy Brukardt følgende:
> That's not allowed, as it would require extra mutual exclusion. Since that 
> exclusion would have to be separate from the protected action (necessary 
> since the entry may not be open when the call is made), you'd also have a 
> race condition (the precondition could be evaluated with one value, the 
> value then changed, and then later the entry accepted). Best practices is 
> always that preconditions should only depend on the parameters to a call 
> (regardless of the kind of call involved).
> 
>                         Randy.
> 
> ....