Menu
▾
▴
Re: [Jmlspecs-interest] JML and concurrency discussions: labels for checking req and ens
|
From: Gary T. L. <le...@cs...> - 2006-09-22 01:18:06
|
Hi Wladimir, and all,
On Thu, 21 Sep 2006, Wladimir de Lara Araujo Filho wrote:
>> This discussion part is about labels for checking pre and
>> postconditions.
>>
>> On Wed, 20 Sep 2006, Wladimir de Lara Araujo Filho wrote:
>>
>>>>>>> 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.
>> ...
>>>>>> [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.
>> ...
>>>>> 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
>>> 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.
>> I'm not really convinced by this example. First the effective
>> precondition of the method is true (the "or" of the two given
>> preconditions).
>>
>> Second, to me it seems that one should require that the objects
>> mentioned in the pre and postconditions, msg and mq, be thread safe.
>> Perhaps this is asking too much, but I don't understand why that's not
>> necessary to prevent external interference in such cases? That is, if
>> we want to do Hoare-style reasoning about a call to a method like, I
>> don't see what good it does to have the method sendAndWait if the
>> caller doesn't have a lock on msg and mq.
> [Wladimir Araujo] I think this is just a communication problem between
> us :) I am not saying that it is not necessary for msg to be thread safe
> (waitqueue is a field). I am saying it is not sufficient. In this
> example I am assuming msg is thread safe (like many designers do when
> they write methods like this but express it loosely [informally]). I do
> agree that for *reasoning* these checkpoints are not necessary (your
> article with Edwin and others develop the subject quite well). However,
> I am targeting *instrumentation*. The RAC cannot know the safe point for
> executing the assertion checking code unless we provide a hint. Model
> checking techniques could be used to do it automatically, or maybe other
> static analysis techniques would do. I am picking, for now, a manual
> one. Maybe later we can try something smarter.
> A little more on the example: although a lock on msg is acquired inside
> the sendAndWait(), msg *is* thread safe (lock_protected, actually) when
> it is passed in when considering external accesses to it. The lock is
> acquired inside the method to preserve this property (and to wait() on
> it, as you can see), otherwise an unprotected access would violate this
> predicate.
Sorry for not understanding more quickly...
If the problem is that the precondition involves hidden data, this
would violate normal rules for the visibility of names mentioned in
the precondition. (See the recent TR by Peter Mueller and me about
information hiding in JML method specfications.) It seems like we
could extend such rules to locking; that is, shouldn't it be possible
for the client to obtain all locks necessary to make evaluating the
precondition
waitqueue.contains(handle);
be threadsafe? That is, should the object provide, to clients, the
ability to lock the object (this) in such a way that waitqueue was
locked? In that case the client could again have all locks needed to
make evaluation of the precondition thread-safe. If this can't be
done, then I don't see how we can impose condition as a precondition.
On the other hand, if the case analysis in the specficiation is just
to make the method specification easier to state, and is not intended
for clients, then the client's precondition is "true" and there is no
problem with that. But then I can see how you might want a point at
which you decide which of the internal postconditions you want to
satsify. This might be better handled by a mechanism such as
specified blocks, which we are supposed to implement in JML, but no
one has done yet (see old discussions on the jmlspecs-interest list).
That is you might rather write something like (using
following_behavior to specify behavior of a block):
/*@ public normal_behavior
requires true;
ensures (* ...... something about ordering guarantees ... *);
when (*... have to state this in terms of model fields *);
@*/
public void sendAndWait(Msg msg, Handle handle)
{
synchronized(msg)
{
synchronized(waitqueue)
/*@ following_behavior
@ requires waitqueue.contains(handle);
@ ensures (*... something about ordering guarantees ...*);
@ when waitqueue.get(handle).front() == msg && msg.hasReply();
@ also
@ following_behaviour
@ requires !waitqueue.contains(handle);
@ ensures ... other ordering guarantees ...
@ when ... same as above ...
@*/
{
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
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
}
Would that kind of thing work for you?
Note that the specified block allows you to tell the RAC when to
evaluate conditions.
(This could be seen as a sugared way of using assume and assert.)
I guess what bothers me is that I'd like to be able to check at least
the public preconditions at the call site, not necessarily at some
place within the body. That's why I was looking for a way to figure
out what had to be thread safe.
> Regarding post-conditions it is reasonable to require that any arguments
> or global (therefore external) objects present in the formula be thread
> safe. Analogously to the pre-condition, this is not sufficient due to
> internal interference.
I wonder if the same kind of argument applies.
>> I wonder if we could require thread safety for all mutable objects
>> that can determine the true value of the pre and postcondtions for
>> a method. Does that cause major problems for concurrency?
> [Wladimir Araujo] It depends. For 99% of the cases, I would say it is
> not a problem. It is actually the intent. The example above falls into
> this category. What I can see being a problem are the cases in which the
> formula references objects that are NOT being manipulated by the method
> or at all read by it. A simple example would be a consistency check in
> which the formula refers to an external state object to verify if the
> method was invoked in an admissible state. Even if the object is thread
> safe the access to it by the formula might not be. In this case, extra
> concurrency control measures would have to be taken to ensure thread
> safety. This has, however, implications on the observability of
> interleavings.
>
> The whole point I am getting at (hopefully) is that although arguments
> and external objects are thread safe, assertion checks based on them and
> internal state can only be performed at certain points INSIDE the method
> being executed because the method itself is going to (ideally) access
> such objects in a thread safe manner only at such points and these
> points cannot be determined internally by a RAC. Therefore we need these
> checkpoint statements for instrumentation.
I think I'm understanding this now. I still wonder if a divsion of these
properties into public specifications (which might even be checked
outside the method's execution and have to hold at the call site to
premit Hoare-style reasoning) and internal (private) specifications,
which may indeed be in-line assertions or specified blocks, might be
all we need. Let me know what you think and if you disagree...
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
|