From: Wladimir de L. A. F. <de...@co...> - 2006-09-20 06:38:48
|
> -----Original Message----- > From: Gary T. Leavens [mailto:le...@cs...] > Sent: September 19, 2006 10:52 PM > To: Wladimir de Lara Araujo Filho > Cc: JML interest list; 'Edwin Rodriguez' > Subject: RE: JML and concurrency discussions > > Hi Wladimir, > > On Sun, 17 Sep 2006, Wladimir de Lara Araujo Filho wrote: > > > After a long summer absence, I'm back with funny questions and > > proposals re concurrency. See my comments inline. > > Thanks... > > > > 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. 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. > > 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? > > >>> The basic idea is to be able to specify \max(lockset) = l1, i.e. > >> the > >>> current thread cannot acquire any locks after acquiring l1. > >> > >> Yes, these should be statically specified. > >> > >> [Wladimir Araujo] ... > > > > Ok. > > > >>> I am also proposing the use of the following labels to mark safe > >> spots > >>> inside a method for the checking of pre and post conditions, namely > >> the > >>> requires_checkpoint and ensures_checkpoint, respectively. They would > >> be > >>> counterparts to the requires and ensures clauses in the same way the > >> commit > >>> label is a counterpart to the when clause. If they are not specified, > >> they > >>> default to the pre and post state of the method in question, which is > >> the > >>> current behaviour. Your comments on this are greatly appreciated. I > >> was also > >>> wondering if labels are the best construct for this. Would a > > statement > >> be a > >>> better choice (they would then become a JML keyword)? > >> > >> I'm not sure I understand why you need these labels. The > >> requires predicate should certainly hold at the call site, the runtime > >> checker should not an error at the earliest possible point in the call > >> of a method if the method's precondition doesn't hold. The > >> postcondition should be true after the method call for the caller's > >> benefit again, it doesn't help the caller if this is checked somewhere > >> in the middle of the method. So I'm not understanding this... > > > >> [Wladimir Araujo] > >> [Wladimir Araujo] The idea is this. To avoid interference between > >> multiple threads when checking the assertion generated code, the > > objects > >> being accessed need to be guaranteed to be properly protected. The > >> simplest approach (which is a no go) is to have a global lock acquired > >> by the RAC when checking any assertion. That doesn't work because it > >> will inherently eliminate thread interleavings that might happen when > >> running the uninstrumented program. The approach I am proposing is to > >> flag the point in the method execution in which it is known (to be > > best > >> of the designer's knowledge) that such objects are properly guarded so > >> that RAC code can execute safely. The issue here is that such locks > > are > >> only acquired (in general) inside the method execution. Worse, they > > (or > >> at least some) are likely to be released before further processing is > >> done inside the method. > >> > >> Yes, I agree that it is a deviation from the original DbC methodology. > >> The idea, however, is to see how much we can still specify using > >> contracts following the original idea augmented with these constructs > > to > >> demarcate safe points. This is a very brief explanation. If you (or > >> anyone) would like more details, please let me know and I can forward > >> you a (very) incomplete thesis proposal that provides examples and > >> discusses the limitations of this approach. > > > > I see. Perhaps one technique would be to require that the caller > > always guarantee thread safety (holding locks or having thread-unique > > references) for all objects needed to evaluate the pre- and > > postconditions. (This is related to independence.) If that is the > > case, the RAC could first test (or assume) this and then test the > > actual predicates. This isn't unreasonable, as if the objects > > involved are not thread safe, then there can be interference by other > > threads that will invalidate the checks made by the RAC. (See our > > ECOOP paper for more about this.) > > > > [Wladimir Araujo] The idea of thread safety for the arguments and any > > _external_ objects referenced in the contracts is implied (I took this > > from your paper). However, this is not enough. Thread safety for > > arguments only protects you against external interference. Internal > > interference needs to be handled, well, internally. These constructs > > demarcate the safe points from internal interference. They say nothing > > about the external aspect, which is assumed to be checked by the > > thread_safe construct for the arguments and any external objects > > referenced in the specifications. Although the method implementation > > (assumed correct, for a moment) provides correct concurrency control, it > > says nothing about the point at which the pre and post condition can be > > evaluated such that they are free from interference and their outcome > > can be related (i.e. satisfying the pre-condition implies that the > > corresponding post-condition is evaluated after the method execution). > > I see. But what if we combine the suggestion about thread safety with > also getting a lock on the object that is the receiver in order to do > checking of pre-and postconditions (or checking that such a lock is > held)? [Wladimir Araujo] Unfortunately, that's not always the case. It is common practice to use different lock objects than the receiver, so locking the receiver would not help. Here is an example (from messaging systems): /*@ normal_behaviour requires waitqueue.contains(handle); ensures ... something about ordering guarantees ... when waitqueue.get(handle).front() == msg && msg.hasReply(); also normal_behaviour requires !waitqueue.contains(handle); ensures ... other ordering guarantees ... when ... same as above ... */ void sendAndWait(Msg msg, Handle handle) { // so stuff here to check validity of msg and state of the system synchronized(msg) { synchronized(waitqueue) { // here is the point I can truly evaluate the // pre-conditions because I have the lock on // all the objects I need MsgQ mq; if(waitqueue.contains(handle)) { // put it in the back of the queue mq = waitqueue.get(handle); mq.enqueue(msg); } else { // create a queue and put it in the front of it mq = new MsgQ(msg); waitqueue.put(handle, mq); } while(mq.front()!=msg) waitqueue.wait(); send(msg); } while(!msg.hasReply()) msg.wait(); // here is the point where the when clause should be satisfied // notice that it is partly satisfied after the prior wait //@ commit: } // read response and handle error conditions // whoever notifies 'msg' when the response arrives // already takes care of updating waitqueue, so this method // does not need to acquire a lock on it anymore } In this case, the receiver object is not a relevant lock, multiple locks are required and the post-conditions will likely need extra locking to be checked. Also notice that the when clause was split in two but at the commit point the lock on the waitqueue (which is required to evaluate part of the formula) is no longer held. Situations like this are not uncommon. What happened to the 'when' can happen to the post-condition (it is actually easier to happen with it). I don't see an alternative other than to explicitly demarcate the assertion checking point. Even then, there will be cases in which the expressions will have to be simplified due to the impossibility (or unwillingness due to performance impacts, etc) of acquiring all necessary locks, like the 'when' above. Again I'd like the rules to be as simple as possible. WOn't > we be able to detect if the method doesn't correctly have concurrency > control by finding that the post-condition isn't satisfied when the > method attempts to return? > > > But perhaps the idea you are exploring is important in some > > circumstances. I would tend to think, however, that by using the > > "when" clause, one could separate the pre-condition into parts that > > must be true to make the call (requires) and parts that the > > implementation will wait for (when). > > (I'm not sure who wrote the above, but I agree. :-) [Wladimir Araujo] That was you :) > > > Perhaps a similar division in > > the postcondition would also be fruitful? > > > > [Wladimir Araujo] As far as I understand, the 'when' clause is not part > > of the pre-condition (we could make it, though). > > Right, it's not part of the precondition. I think it should remain > separate. > > > Once the pre-condition > > is evaluated, the post-condition to be satisfied is already determined > > independently of the 'when'. > > Yes. > > > In other words, in the following method > > specification > > > > /*@ > > normal_behaviour > > requires P; > > when Q; > > ensures W; > > also > > normal_behaviour > > requires P2; > > when Q2; > > ensures W2; > > */ > > void m(); > > > > once P is satisfied, it is expected that W is guaranteed, independently > > of Q. > > Yes. > > > The 'when' clause to be evaluated is actually determined by the > > pre-condition. So, if P is true, 'm' is expected to block until Q is > > satisfied and it will guarantee W to its caller. > > Yes. > > > Alternatively, if P2 is > > satisfied, 'm' will block until Q2 is satisfied and guarantee W2 to its > > caller. > > Yes. > > > So, I see the 'when' clause (at least as it is today) more like a > > post-condition. > > I don't agree. > > > Furthermore, once the 'when' clause is satisfied, no > > more blocking is allowed, so it is "physically" closer to the > > post-condition than to the pre-condition. > > I don't believe that more blocking is not allowed, it depends if the > method is supposed to be commit-atomic or not. [Wladimir Araujo] I didn't know a 'when' could come without a 'commit'. I understood from your article that when it is omitted, the commit point is assumed to be at the end of the method. > > > This is just to say that depending on what is being described, the > > "when" clause can be seen as part of the pre-condition or as part of the > > post-condition. > > It's really neither, but it could be used that way, as you show... > > > An example of the former is a producer-consumer scenario > > in which you have to wait for items to be available (the "when" clause) > > to take them. An example of the latter is an RPC system in which you > > need to wait for a response to be available to take it (i.e. to return > > from the method). In both cases the "when" clause absorbs > > responsibilities from the pre- and post-conditions, respectively. > > Yes, that's possible. > > > Thus, I don't think at the moment that we need another clause. I do find > > the idea interesting, though. I will keep it in mind. > > Ok. Thanks for thinking these things through. [Wladimir Araujo] Thank you for listening and posing interesting questions. > > 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 |