Taken for Granted

ESL, embedded processors, and more

The return of “design by contract”

Filed under: Uncategorized — May 11, 2009 @ 8:00 pm

One of the very interesting sessions I saw at DATE 2009 a couple of weeks ago was a panel session on Wednesday 22 April: Session 8.1, Architectures and Integration for Programmable SoCs. During this session, Axel Jantsch of KTH in Sweden made a couple of interesting comments:

2010-2020 will be the golden age for SoC architects

and he also suggested, complementing a comment by Pieter Mosterman of the Mathworks (who talked about compositional design) that IP integration in SoCs might be handled using Device Level Interfaces and “design by contract” (where the conformance of blocks and the whole SoC to the Device Level Interfaces forms part of the contract).

There is a lot that makes sense about this idea for IP integration into complex SoCs. Equally interesting to me was that Axel’s comment plunged me into a wave of nostalgia about Bertrand Meyer (also his home page here) and the “Design by Contract” he was talking about in the mid-1980′s in software development. In his Eiffel language, he used the idea of preconditions and postconditions on function calls that could be used to check whether the interfaces satisfied the assumptions and constraints (the “contract” between the caller and callee). In essence and explicitly, this is a kind of assertion checking. Eiffel supported the idea that you could keep the assertion checking in while developing the system, and then for production purposes, when you were “sure” that the code was correct, you could compile them out. (if you were ever sure).

No caption necessary, I hope!

I remember to this day a talk Bertrand Meyer gave at the Bell-Northern Research auditorium at the Carling facility in Nepean, near Ottawa, in the mid-to late 1980s about his ideas, which I had not heard of before. We also all got a copy of his Eiffel book, “Object-oriented Software Construction” (Prentice-Hall, 1988 – the link is for the 2nd edition, 1997) and it was a very stimulating time for me, learning about some of these new ideas.

Bertrand Meyer later wrote a very interesting column in IEEE Computer about the Ariane 5 disaster (see here for a slightly different version, with discussion) and pointed out that this was a contract failure – that assumptions implicitly made about reused software were explicitly violated in the new system context. A graphic example pointing out the usefulness of these ideas (thankfully, with only an economic cost, not a cost in human life).

It is most interesting to see the ideas come around again. You can’t keep good ideas down!

5 Comments »

  1. Perry Alexander:

    This is exciting! I still think the the design-by-contract approach is wonderful. It played an essential role in the design of Rosetta’s component system where one defines usage conditions and guaranteed properties for each component, and verifies them during composition. I think design-by-contract had significant influence on software development even though its formal adoption was widespread. I wonder why that was not the case? Along the same lines, the Larch interface language concept is also worth a look.

  2. Jakob Engblom:

    I remember learning Eiffel as an undergrad, and thinking it was pretty neat but a bit clunky. Part of the issue was their use of a programming environment that was pretty slow on our shared Sun servers… and with a graphics environment that was less than ideal.

    My general experience, though, with pre/postconditions is that for non-trivial code or stateful code, they quickly become too hard to do. Sure, if you compute something fairly cleanly, you are fine. But if the function is to “update remote SQL database with information about user, possibly concurrently with actions from a parallel session of the same user’s”, pre/postconditions end up being crazy. Or trivially meaningless.

    Most real code is not computing function or doing simple steps, it is doing massive amount of state change.

    Even as simple as driving a TLM transaction from a processor to a device gets very complex — and what is the post-condition? That the transaction arrived? That it computed the right thing? That the conditions inside the device are satisfied? And how do you describe, in a simple way, “after writing this register, the virtual CPU will see an interrupt in 1037 cycles, unless it polls me”…

    It is simply very hard considering the high level of modern software to do reasonable conditions.

    /jakob

  3. Grant Martin:

    Jakob – an interesting comment regarding your experience with Eiffel. However, the idea of “design by contract” may remain even if the form of contract specification and auditing is quite different than the simplistic mechanisms that you point out are very hard to implement with complex state-based systems. Nevertheless, the progress made in property specifications and assertion based design in verification (at least for classes of embedded systems) seems to me to indicate that checking complex “contracts” is possible in at least some classes of interesting systems. The TLM2 compliance checking tools from Jeda seem to be a form of this idea (see http://www.jedatechnologies.net/base/). And property specification mechanisms for assertions, such as PSL, actually do allow you to specify something like “after writing this register, the virtual CPU will see an interrupt in 1037 cycles, unless it polls me” – albeit, perhaps not in such a simple way.

    This then gets into debates about what “real code” is doing, and whether the implicit “contracts” involved in real code can be decomposed into at least some checkable assertions that will guard against at least some classes of errors. In other words, even if the design by contract concept is not the holy grail that prevents all errors ….. can thinking in this way, and applying it using whatever technical means are available, improve design, implementation and verification?

    I have seen plenty of examples of real code where an application of more thinking about what each step is doing when the task is being decomposed, and what the underlying “contractual assumptions” are, would have helped produce more robust systems with fewer errors. (and not all real code is doing a “massive” amount of state change).

  4. Jakob Engblom:

    It is an attractive idea, and for localized issues like checking TLM2 protocol compliance, it can certainly work. However, I am more concerned about the larger picture, where it feels that the assertions will be just as complex as the code they will check.

    The idea of assertions to me is that the functionality of a function can be expressed in some much more compact way than the function’s code. For something like sorting a list, that is obviously feasible. But for larger-scale behaviors, it is less obvious. Maybe for data plane processing it is more feasible than control-plane code or user interfaces.

    There was a good discussion in teh StackOverflow podcast #53 about unit testing which is essentially the same problem, listen to it at http://blog.stackoverflow.com/2009/05/podcast-53/ . Three very experienced programmers discuss their experience with unit tests and why and when they may or may not work.

  5. Jakob Engblom:

    Please edit the previous post… last sentence came out really strange.

    “Three very experienced programmers discuss their experience with unit tests and why and when they may or may not work. ”

    Is a better phrasing.

RSS feed for comments on this post. TrackBack URI

Leave a comment

Line and paragraph breaks automatic, e-mail address never displayed, HTML allowed: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>

(required)

(required)