Re: [Jmlspecs-interest] JML and concurrency discussions: locking order specification

[Gary T. L. <le...@cs...>]

Hi Wladimir, and all,

(I'm trying to break this discussion up into smaller topics...)

I think we agree about having a clause like lock_order.

On Wed, 20 Sep 2006, Wladimir de Lara Araujo Filho wrote:

>>> In summary, the locking invariant allows the local specification of
>>> locking policies with global effects. I don't know if this is an
>>> advantage or disadvantage. I can imagine it makes reasoning more
> complex
>>> but it is more intuitive to use.
>>
>> This seems like it might be a sensible thing to do.  But I wonder if a
>> static set of ordering declarations would still work and be easier to
>> reason about.  E.g., some syntax like
>>
>>      //@ lock_order a < b;
>>
>> or some such.  These would replace the current use of axioms.

> [Wladimir Araujo] This is what I intended, actually. The only important
> point is to have the notions of scope and "in effect" for the locking
> assertions as to get away from the inconsistencies of axioms while
> having an intuitive notation.

Ah, okay.  Then I think we basically agree...

>> It
>> seems like if these kind of declarations are mixed in with general
>> logical statements.  In your example you use:
>>
>>     "this < a && this < b && b <= a"
>>
>> which seems fairly easy to pull apart, but if these are general
>> logical formula, then they could be come arbitrarily complicated, as
>> in
>>
>>    !(a <= this ==> this < b)
>>
>> from which recognizing the lock ordering would require (at worst)
>> theorem proving.  Certainly that is more flexible, but I wonder if the
>> flexibility is needed in practice?

> [Wladimir Araujo] You have a very good point. This flexibility is not
> needed in general. I haven't seen any such case in the systems I work
> with. Locking policies are usually simple to explain (verbally) and thus
> should be simple to express. The implied universal quantification does
> the job. One to many and many to one relationships between objects are
> easily covered by placing the locking assertion on the side of the many
> as long as the one is reachable from it. It is very important to be able
> to specify policies like "I can only lock the object if I locked its
> container first". This policy can be put on the contained as long as the
> container can be referenced from it. Otherwise we'll need a universal
> quantifier, implicit through a collection (a JMLCollection) or explicit
> over the elements of a collection.

Ok, seems like we agree on this.  That is we both seem to want a
simple caluse that can be easily statically analyzed.

>> It's also not clear how to prevent non-locking information from
>> getting into these invariants.  Again a more restricted syntax that
>> only declares orderings would perhaps solve the problem.

> [Wladimir Araujo]
> We could have something like:
>
> //@ lock_order a < b, b < c, d <=e, \max(set1) < r, t < set2
>
> The commas are replacements for "&&" to eliminate the idea of a logical
> formula. Set1 and set2 are instances of JMLCollection. Being a modeling
> type, a JMLCollection cannot be used as a lock object itself, so there
> are no ambiguities in the expression "t < set2", which always means t <
> 'elements of set2'.
>
> What do you say?

That seems good to me.

         Gary T. Leavens
         Department of Computer Science, Iowa State University
         229 Atanasoff Hall, Ames, Iowa 50011-1041 USA
         http://www.cs.iastate.edu/~leavens  phone: +1-515-294-1580