rodin-b-sharp-devel

[Rodin-b-sharp-devel] IProofCommand and concurrency

[Matthias S. <Mat...@in...>]

Dear list,

I implemented an instance of IProofCommand and am now trying to 
eliminate race conditions.

Is it possible that the objects referenced by IUserSupport are modified 
concurrently during execution of apply?
Is it possible that the objects referenced by IUserSupport are modified 
between execution of isApplicable and apply?

Thanks for your help,
Matthias

Re: [Rodin-b-sharp-devel] IProofCommand and concurrency

[Laurent V. <lau...@sy...>]

Dear Matthias,

Le 6 mai 2011 à 09:09, Matthias Schmalz a écrit :

> I implemented an instance of IProofCommand and am now trying to 
> eliminate race conditions.
> 
> Is it possible that the objects referenced by IUserSupport are modified 
> concurrently during execution of apply?

No, apply is atomic.  The user support will not change concurrently.

> Is it possible that the objects referenced by IUserSupport are modified 
> between execution of isApplicable and apply?

This is currently not the case, as far as I know.  However, you should not rely on it and cache any information in between the two calls.

More generally, the assumption in the Rodin API is that, unless otherwise stated, all method invocations are atomic and there is no guarantee between method calls, so that clients should never cache information.

Cheers,
Laurent.

Re: [Rodin-b-sharp-devel] IProofCommand and concurrency

[Matthias S. <Mat...@in...>]

All right. Good convention.

Am 06.05.2011 11:47, schrieb Laurent Voisin:
> Dear Matthias,
>
> Le 6 mai 2011 à 09:09, Matthias Schmalz a écrit :
>
>> I implemented an instance of IProofCommand and am now trying to
>> eliminate race conditions.
>>
>> Is it possible that the objects referenced by IUserSupport are modified
>> concurrently during execution of apply?
>
> No, apply is atomic.  The user support will not change concurrently.
>
>> Is it possible that the objects referenced by IUserSupport are modified
>> between execution of isApplicable and apply?
>
> This is currently not the case, as far as I know.  However, you should not rely on it and cache any information in between the two calls.
>
> More generally, the assumption in the Rodin API is that, unless otherwise stated, all method invocations are atomic and there is no guarantee between method calls, so that clients should never cache information.
>
> Cheers,
> Laurent.
>