From: <Cle...@so...> - 2006-09-22 09:30:12
|
Hi everyone, I'm a Phd student of Marieke Huisman and I'm very interested in what you'= re=20 talking about. I've reviewed the ecoop paper and the classes annotated with= =20 the new jml keywords (spex project). I've found that many of the classes ha= ve=20 the same defect that you're pointing here: it is more difficult to write=20 correct specifications in a multi-threaded context, because one has to take= =20 care about internal and external interference. Properties appearing in=20 postconditions hold often only within the body of the method, and becomes=20 false because of external interferences. Often in spex classes, specifications records the state of the heap with = old=20 construct and reuses it in the postcondition. Here is an example: /*@ public behavior @ locks this.putLock_; @ when !this.isEmpty(); @ ensures \result =3D=3D \old(head.next.value) && \old(head.next).v= alue =3D=3D=20 null; @ signals (Exception ie) ie instanceof InterruptedException; @*/ public /*@ atomic @*/ Object take() { Object x =3D extract(); if (x !=3D null) return x; else {=20 synchronized(putLock_) { try { ++waitingForTake_; for (;;) { /*@ commit: @*/ x =3D extract(); if (x !=3D null) { --waitingForTake_; return x; } else { putLock_.wait();=20 } } } catch(InterruptedException ex) {=20 --waitingForTake_;=20 putLock_.notify(); throw new RuntimeException();=20 } } } } As far as I know, \old(head.next.value) is evaluated after arguments are=20 passed to the method. In that case, since this method does not acquire any= =20 lock, it can be interrupted before the first line ("Object x =3D extract()"= ).=20 At that point, the state of the queue can changed completely (multiple take= ()=20 and put() can occur, thus deprecating \old(head.next.value) ). Am I correct= ? In my opinion, this is a variant of your conclusions: > > 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... Generaly, in a multi-threaded context, properties, from the caller point of= =20 view, are weaker. Moreover, properties hold only within the body of a metho= d.=20 Thus, I agree.. Cl=E9ment |