SCOOP: Do wait - ever conditions for expire
Alejandro Garcia
which is elegant, but raises a question I haven't found addressed in the literature:
Do wait-for conditions ever expire, or does a processor wait indefinitely as long as the program is running?
If the latter, has anyone developed a pattern for enforcing a timeout or expiry on them?
Alejandro
https://elviejo79.github.io
Too brief? Here's why! https://www.emailcharter.info
EOM – End Of Message. The whole message is in the subject don't need to open it.
NNTR – No Need To Respond. Help cut down on all those “cool” and “thanks” emails.
SINGLE SUBJECT. Send one email for one topic, this makes replies easy..
CLEAR CALL TO ACTION: Ask for some specific result very clearly.
Eric Bezault
I'm not aware of such thing. But if that was possible, do we
agree that when such timeout would occur, the precondition
would stop playing its role of wait-condition and raise a
precondition violation exception as for non-SCOOP preconditions?
--
Eric Bezault <er...@gobosoft.com>
Eiffel expert - available for freelance work
https://www.gobosoft.com
On 13/06/2026 4:19, Alejandro Garcia wrote:
> In SCOOP, preconditions become wait-for conditions rather than assertions
> which is elegant, but raises a question I haven't found addressed in the
> literature:
>
> Do wait-for conditions ever expire, or does a processor wait
> indefinitely as long as the program is running?
>
> If the latter, has anyone developed a pattern for enforcing a timeout or
> expiry on them?
>
> Alejandro
>
> --
> Alejandro García F. (elviejo)
>
>
> Too brief? Here's why! https://www.emailcharter.info <http://
> emailcharter.org>
> open it.
> NNTR – No Need To Respond. Help cut down on all those “cool” and
> “thanks” emails.
> SINGLE SUBJECT. Send one email for one topic, this makes replies easy..
> CLEAR CALL TO ACTION: Ask for some specific result very clearly.
>
> You received this message because you are subscribed to the Google
> Groups "Eiffel Users" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to eiffel-users...@googlegroups.com <mailto:eiffel-
> users+un...@googlegroups.com>.
> To view this discussion visit https://groups.google.com/d/msgid/eiffel-
> users/
> CALFgaYCdjy4pYBX2T_X7makrMNFO_ac7%2BePdGBZqaPfCPjcCSw%40mail.gmail.com
> <https://groups.google.com/d/msgid/eiffel-users/
> CALFgaYCdjy4pYBX2T_X7makrMNFO_ac7%2BePdGBZqaPfCPjcCSw%40mail.gmail.com?
> utm_medium=email&utm_source=footer>.
Miguel Oliveira e Silva
IMHO, a separate precondition [1] cannot (ever) became a normal (sequential) assertion because it would be a race-condition. If such a timing constraint failure is to be implemented then an explicit timing condition should part of the routine contract.
If the precondition is the choice for such timing constraint (as we would infer it would, if the precondition recovers its sequential behavior), then which client should be responsible for the failure (thus, targeted with the proper launched exception)?
The one waiting? Or the "one[s]" that did not ensured a valid precondition? In a perfect world, the latter should be the choice, but that's impossible: we have no reference to it and, in fact, most likely it is not a client of the routine. As such, if such contract is to be ensured in the precondition, then the waiting client should be targeted, and a defensive programming approach should be taken in that client.
However, there are, IMHO, other (better) alternatives. For starters, the responsibility should lie in the routine, not on its client. Thus, it should not be part of its precondition.
For quite some time I've been thinking and working on an extension of DbC for timing constraints (an OO language approach for real-time programming was the initial motivation). (I have a MSc student that has proved the concept in a practical implementation, and, as we "speak", is working on the thesis writing).
Programs normally express algorithms from a pure logical perspective. Although some synchronization/order between some of the program elements is imposed, it does so regardless of the execution time involved (being attoseconds, or the age of the universe are, in this perspective, irrelevant).
However, timing constraints are not irrelevant in practical programs, and, of course, are critical in (hard) real-time programming (as are processor scheduling, memory handling, shared resources, priorities, and other system level requirements).
Time is always relative (even in classical Newton physics). We need a reference to make a time value meaningful. In a program, we could use an absolute external clock; the program execution time; or, the routine execution time. Clearly, the latter one, is the best choice for expression timing constraints.
So, if a language abstracts and implements a special integer query -- elapsed_time (Duration?)-- representing the current routines execution time (starting at its invocation, not its body execution) then predicates can be formed to express deadline requirements or timeouts for handling a request.
However, as suggested before, preconditions are not the proper assertion to place such a contract. Postconditions would be the immediate alternative. But what is the meaning of a postcondition before the routine executes its body? (I remember some discussion on this matter 20 years ago at CORDIE'06 at York, UK.)
Preconditions, postconditions and class invariants are discrete assertions, they only apply in discrete times in the program execution (before, after routine execution, and at stable times in the object lifetime). For practical useful applications, timing constraints should be applied continuously (or else, for example a missed deadline would be detected to late, if ever, for a proper failure handling).
Thus we propose a new kind of contract: routines invariants. Unlike class invariants, a routine invariant (as its name strongly suggests) is a continuous predicate applicable across routine's execution. Adapting an example from [https://www.eiffel.org/doc/solutions/Producer-consumer]:
store (a_buffer:
separate BOUNDED_BUFFER [INTEGER]; an_element: INTEGER; timeout:
INTEGER)
-- Store `an_element' into `a_buffer'.
invariant
elapsed_time < timeout
require
not a_buffer.is_full
do
a_buffer.put (an_element)
ensure
not a_buffer.is_empty
a_buffer.count = old a_buffer.count + 1
end
Here, as it should, a timeout is the responsibility of the routine, not the client, and there is no hidden contract.
Routine's invariants could also be very useful to express frame conditions (what never changes), and other logical predicates (for instance, ensure that the temperature of a boiled is always within a given interval).
Perhaps a (much stronger) continuous variation of class invariants could also be considered (across invariant ?).
Best regards,
-miguel
[1] I have a slightly different view of this type of assertions. I named then concurrent assertions, applicable to any type of assertion: preconditions, postconditions, checks, and invariants. A concurrent condition -- which within an assertion, becomes a concurrent assertion -- is a predicate whose value may depend on a different processor (active entity) than the one testing the predicate [PhD thesis, 2007, chapter 5, section 1.2, https://sweet.ua.pt/mos/pubs/phd-thesis_en.pdf]. (Please note that this document is a draft translation of my thesis -- at the time, written in Portuguese -- so translation errors may definitely exist.)
In my MP-Eiffel concurrent proposal, concurrent conditions not only express concurrent assertions (with the safe behavior of, when necessary, being a conditional synchronization application), but also express external synchronization, when used in conditional instructions (as with concurrent assertions, any other behavior would be a race-condition).
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/eiffel-users/ef508895-69aa-41e1-b1a6-a6687ce2ef27%40gobosoft.com.
-- Miguel Oliveira e Silva IEETA-DETI, University of Aveiro, Portugal
Eric Bezault
> Thus we propose a new kind of contract: routines invariants. Unlike
> class invariants, a routine invariant (as its name strongly suggests) is
> consumer]:
>
> store (a_buffer: separate BOUNDED_BUFFER [INTEGER]; an_element: INTEGER;
> elapsed_time < timeout
> * require
> do
> a_buffer.put (an_element)
> ensure
> not a_buffer.is_empty
> a_buffer.count = old a_buffer.count + 1
> end
>
> Here, as it should, a timeout is the responsibility of the routine, not
> the client, and there is no hidden contract.
It's not clear in your example above.
Miguel Oliveira e Silva
In the routine contract, the Client has the new benefit of a routine
invariant (no extra obligation); and the Supplier has the new obligation
of ensuring the routine's invariant (no extra benefit).
A rescue clause can be attached in the desired level to handle the
problem (if a deadline was missed, perhaps retry requiring less
computational work, or/and using weaker timing requirements, or whatever
the problem prescribes as solution or workaround to the problem). In a
real-time problem most likely there will be different deadlines, leaving
the more strict, critical, and unrecoverable deadline to last in a chain
of rescue clauses.
-miguel
> You received this message because you are subscribed to the Google
> Groups "Eiffel Users" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to eiffel-users...@googlegroups.com.
> To view this discussion visit
Eric Bezault
(apart from the continuous vs discrete aspect) is that on failure
the corresponding exception may be caught by the routine (in
its rescue clause). But if there is no rescue clause (or no `retry`
in it), then how is it different from a precondition violation?
The call might be asynchronous and the client of the call
might not ready anymore to handle such exception. So I understand
the rationale to let the routine have a chance the handle the
exception, but if it does not then we're back to your initial
criticism about turning the wait condition into a regular
precondition violation after some timeout. Or did I miss something?
--
Eric Bezault <er...@gobosoft.com>
Eiffel expert - available for freelance work
https://www.gobosoft.com
Miguel Oliveira e Silva
the client, not the supplier (routine). If a client, when calling a
routine, receives a precondition exception it should assume that it is
its fault (or else, the mechanism looses its power and simplicity), not
the supplier fault.
The failure should be rescued (if desired) at whatever level the
programmer considers it appropriate. In the example given, not in the
failed routine because timeout is a (readonly) argument; so once failed,
that invariant will never be recoverable by that routine (perhaps at an
upper routine level)
If the call is asynchronous, the problem is similar to other causes for
routine failure (postconditions, internal failures, or class
invariant). At the language level the exception should be propagated to
that called whenever it tries to use again the object (asynchronous
exception).
For the example given, we could handle that specific invariant violation
in the routine's rescue clause, as long as we remove the timeout
argument, and pass it (for example) for a class attribute, allowing to
change its value in the rescue clause (a routine can only succeed if the
contract is met).
(Preconditions and routine invariants have very different meanings.)
-miguel
Alejandro Garcia
When considering these questions, I often look at the HTTP protocol for analogies, where 400-level errors represent precondition violations and 500-level errors represent postcondition violations.
Under this framework, we can see a clear distinction:
- 504 Gateway Timeout: The upstream server failed to respond in time (a supplier failure).
- 408 Request Timeout: The client took too long to send the request (a client failure).
This suggests that a timeout is actually a postcondition violation. In a real-world context, this is analogous to a supplier failing to fulfill an order according to a Service Level Agreement (SLA). Therefore, with our current tools, a postcondition violation seems like the better approach.
Miguel asked: "What is the meaning of a postcondition before the routine executes its body?" In the case of a timeout, the meaning is that we could not fulfill the request within the committed timeframe. In a 'rescue' scenario, the supplier has more information to determine the next step—whether to treat it as a "fire and forget" command, retry the operation, or forward the exception to the client.
If we were to add "routine invariants," as Miguel proposes—or "warranties," as I prefer to call them—we could formally include the concept of a timeout as part of the supplier's SLA.
https://elviejo79.github.io
Miguel Oliveira e Silva
Yes, a timeout is a routine failure. However, a routine may fail for reasons other than a false postcondition. It can fail from an internal algorithm failure (failed: check, loop invariant/variant, internal call to another/same routine, ...). None of these are in the routine's postcondition (nor should it be, because the postcondition applies only to the abstract behavior of the routine, not to how it is implemented).
Again, formally a postcondition (Q) applies only after routine (S) termination:
{P} S {Q} -- Hoare triple (P: precondition)
Be definition, a timeout occurs before/during the execution of routine S.
From a practical point of view, we would have huge problems to implement timeouts in the postcondition. What is the meaning of testing a postcondition before routine termination? Should we test only part of it? Which part, and how can we select it? Should we have a special variant of a postcondition to be always applied? (Sure; but lets give it the proper formal name: routine invariant; and allow its application for other useful and insightful purposes than just timeouts.)
Hence, a timeout specification in the postcondition is not, IMHO, the correct contract for the routine.
BTW, a timeout may result from the logic of the program being developed (for instance, the selected number of frames per second in a video application), and not from an independent, external judge. Also, timeouts might be determined by the runtime availability of computational resources (number of cores and their speed, memory availability and its speed and bandwidth), Thus, a separate configuration to determine the timeout of specific routines is not, IMHO, the proper solution.
-miguel
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/eiffel-users/CALFgaYAecQmDj%3DXWW46Rb%2B_UrmXiLb0UJeoXLFYsTr-psnxPeg%40mail.gmail.com.