Runtime verification in Erlang by using contracts

About this paper

Runtime verification in Erlang by using contracts, L.-A. Fredlund et al, presented at WFLP 2018.

Notes

Spoiler alert, but the conclusion to my book OOP the Easy Way is that we should have independently-running objects, like we do in Erlang. We should also document the contract between an object and its collaborators, like we do in Eiffel. The concurrency is there because processors are getting wider, not faster, and applications are becoming more distributed across IOT, “edge compute”, and servers. The contracts are there because we want to tame that complexity, tell people how each of the bits of our system can be composed, and what to expect if they try that. And we want to verify that documentation automatically, keeping ourselves honest.

As the authors here note, Erlang already has good facilities for recovering from errors, but that’s only really suitable for errors that are “things that might go wrong”. Programmer mistakes – call them bugs, logic errors, whatever – are things that shouldn’t go wrong, and Erlang doesn’t help there. Eiffel has really good tools for dealing with things that shouldn’t go wrong.

This paper introduces Erlang Design by Contract, which adds the relevant Eiffel bits to Erlang. At its core is a contract specification that’s richer than that found in Eiffel, allowing developers to assert that particular functions are pure, that they complete within given time, or that a recursive algorithm is trending towards completion.

The bit that achieves our aim, of combining the parallelism of Erlang with the safety of Eiffel, is the cpre/3 function, for implementing concurrent preconditions. The server inspects a message, the sender (from), and its internal state, and decides either to handle the message or queue it for later, changing the server state as appropriate.

In this way, preconditions act not as assertions that trigger failure, but as wait conditions that say when an object is ready to handle a message. The Concurrency Made Easy project found this too, when they built SCOOP, which works the other way and adds concurrency to Eiffel.

EDBC and SCOOP are two very different approaches that start from different places and aim for the middle. It’s really interesting to see that there is common ground: that “precondition as wait” arises whether you add concurrency to contracts, or contracts to concurrency.

Mach and Matchmaker: kernel and language support for object-oriented distributed systems

About this paper

Mach and Matchmaker: kernel and language support for object-oriented distributed systems
, Michael B. Jones and Richard F. Rashid, from the proceedings of OOPSLA ’86.

Notes

Yes, 1986 was a long time ago, but the topics of Mach and Matchmaker are still relevant, and I find it interesting to read about its genesis and development. I also find that it helps me put today’s uses – or abandonments – in context.

Mach

Two main families of operating systems under development today are still based on the CMU Mach project. Let’s get discussing the HURD out of the way, first. The HURD is based on GNU Mach, which is itself based on the University of Utah’s Mach 4.0 project. GNU Mach is a microkernel, so almost all of the operating system facilities are provided by user-space processes. An interesting implication is that a regular user can create a sub-HURD, an environment with a whole UNIX-like system running within their user account on the host HURD.

Not many people do that, though. HURD is very interesting to read and use, but didn’t fulfil its goal of becoming a free host for the GNU system that made it easy to support hardware. Linux came along, as a free host for the GNU system that made it worthwhile to support hardware. I enjoy using the HURD, but we’ll leave it here.

…because we need to talk about the other operating system family that uses Mach, macOS/iOS/watchOS/tvOS/whatever the thing that runs the touchbar on a Macbook Pro is called OS. These are based on CMU Mach 2.5, for the most part, which is a monolithic kernel. Broadly speaking, Mach was developed by adding bits to the 4.2 (then 4.3) BSD kernel, until it became possible to remove all of the BSD bits and still have a working BSD-like system. Mach 2.5 represents the end of the “add Mach bits to a BSD kernel” part of the process.

Based on an earlier networked environment called Accent, Mach has an object-oriented facility in which object references are called “ports”, and you send them messages by…um, sending them messages. But sending them messages is really hard, because you have to get all the bits of all the parameters in the right place. What you need is…

Matchmaker

Originally built for Accent, Matchmaker is an Interface Definition Language in which you describe the messages you want a client and server to use, and it generates procedures for sending the messages and receiving the responses in the client, and receiving the messages and sending the responses in the server.

Being built atop Mach, Matchmaker turns those messages into Mach messages sent between Mach ports. What Mach does to get the messages around is transparent, so it might take a message on one computer and deliver it to a server on a different computer, maybe even running a different architecture.

That transparency was a goal of a lot of object-oriented remote procedure call systems in the 1990s, and by and large fell flat. The reason is Peter Deutsch’s Eight Fallacies of Distributed Computing. Basically you usually want to know when your message is going out over a network, because that changes everything from how likely it is to be received, how likely you are to get a response, to how expensive it will be to send the message.

Matchmaker supported C, Common LISP, Ada, and PERQ Pascal; Accent and Mach messages, and a bunch of different computer architectures. Unfortunately it supported them all through specific knowledge of each, and the paper described here acknowledges how difficult that makes it to work on and proposes future work to clean it up. It’s not clear that future work was ever done; modern Machs all use MIG, an “interim subset” of Matchmaker that only supports C.

Object-oriented design

In my book OOP the Easy Way, I explore the idea that objects are supposed to be small, independent computer programs that communicate over the loosely-coupled channel that is message-sending. Mach and Matchmaker together implement this design. Your objects can be in different languages, on different computers, even in different host operating systems (there were Mach IPC implementations for Mach, obviously, but also VAX Unix and non-Mach BSD). As long as they understand the same format for messages, they can speak to each other.

Consider a Cocoa application. It may be written in Swift or Objective-C or Objective-C++ or Python or whatever. It has a reference to a window, where it draws its views. The app sees that window as an Objective-C object, but the app doesn’t have a connection to the framebuffer to draw windows.

The Window Server has that connection. So when you create a window in your Cocoa application, you actually send a message to the window server and get back a port that represents your window. Messages sent to the window are forwarded to the window server, and events that happen in the UI (like the window being closed or resized) are sent as messages to the application.

Because of the way that Mach can transparently forward messages, it’s theoretically possible for an application on one computer to display its UI on another computer’s window server. In fact, that’s more than a theoretical possibility. NeXTSTEP supported exactly that capability, and an application with the NXHost default set could draw to a window server on a different computer, even one with a different CPU architecture.

This idea of loosely-coupled objects keeps coming up, but particular implementations rarely stay around for long. Mach messages still exist on HURD and Apple’s stuff (both using MIG, rather than Matchmaker), but HURD is tiny and Apple recommend against using Mach or MIG directly, favouring other interfaces like XPC or the traditional UNIX IPC systems that are implemented atop Mach. Similarly, PDO has come and gone, as have CORBA and its descendents DSOM and DOE.

Even within the world of “let’s use HTTP for everything”, SOAP gave way to REST, which gave way to the limited thing you get if you do the CRUD bits of REST without doing the DAP bits. What you learn by understanding Mach and its interfaces is that this scheme can be applied everywhere from an internet service down to an operating system component.

Research Watch, and Java by Contract

I introduced Java by Contract, a tool for building design-by-contract style invariants, preconditions and postconditions in Java using annotations. It’s MIT licensed, contributions are welcome, and I hope this helps lots of people to introduce stronger correctness checking into your software. And book office hours if you’d like me to help you with that.

Java by Contract came about as part of Research Watch, a new blog series over at The Labrary where I talk about academic work and how us “practitioners” (i.e. people who computer who aren’t in academia) can make use of the results. The first post considers a report of Teaching Quality Object-Oriented Programming to computer science students.

By the way, I will be speaking at Coventry Tech Meetup on 10th January on the topic “Beyond TDD”, and Java by Contract will make an appearance there.

Long-time SICPers readers will remember Programming Literate, a Tumblr discussing results from empirical software engineering. And if you don’t, you’ll probably remember your feeds exploding on July 15, 2013 when I imported all of the posts from there to here. You can think of Research Watch as a reboot of Programming Literate. There’ll be papers new and vintage, empirical and opinionated, on a range of computing topics. If that sounds interesting, subscribe to the Labrary’s RSS feed.

Cleaner Code

Readers of OOP the easy way will be familiar with the distinction between object-oriented programming and procedural programming. You will have read, in that book, about how what we claim is OOP in the sentence “OOP has failed” is actually procedural programming: imperative code that you could write in Pascal or C, with the word “class” used to introduce modularity.

Here’s an example of procedural-masquerading-as-OOP, from Robert C. Martin’s blog post FP vs. OO List Processing:

void updateHits(World world){
  nextShot:
  for (shot : world.shots) {
    for (klingon : world.klingons) {
      if (distance(shot, klingon) <= type.proximity) {
        world.shots.remove(shot);
        world.explosions.add(new Explosion(shot));
        klingon.hits.add(new Hit(shot));
        break nextShot;
      }
    }
  }
}

The first clue that this is a procedure, not a method, is that it isn’t attached to an object. The first change on the road to object-orientation is to make this a method. Its parameter is an instance of World, so maybe it wants to live there.

public class World {
  //...

  public void updateHits(){
    nextShot:
    for (Shot shot : this.shots) {
      for (Klingon klingon : this.klingons) {
        if (distance(shot, klingon) <= type.getProximity()) {
          this.shots.remove(shot);
          this.explosions.add(new Explosion(shot));
          klingon.hits.add(new Hit(shot));
          break nextShot;
        }
      }
    }
  }
}

The next non-object-oriented feature is this free distance procedure floating about in the global namespace. Let’s give the Shot the responsibility of knowing how its proximity fuze works, and the World the knowledge of where the Klingons are.

public class World {
  //...

  private Set<Klingon> klingonsWithin(Region influence) {
    //...
  }

  public void updateHits(){
    for (Shot shot : this.shots) {
      for (Klingon klingon : this.klingonsWithin(shot.getProximity())) {
        this.shots.remove(shot);
        this.explosions.add(new Explosion(shot));
        klingon.hits.add(new Hit(shot));
      }
    }
  }
}

Cool, we’ve got rid of that spaghetti code label (“That’s the first time I’ve ever been tempted to use one of those” says Martin). Incidentally, we’ve also turned “loop over all shots and all Klingons” to “loop over all shots and nearby Klingons”. The World can maintain an index of the Klingons by location using a k-dimensional tree then searching for nearby Klingons is logarithmic in number of Klingons, not linear.

By the way, was it weird that a Shot would hit whichever Klingon we found first near it, then disappear, without damaging other Klingons? That’s not how Explosions work, I don’t think. As it stands, we now have a related problem: a Shot will disappear n times if it hits n Klingons. I’ll leave that as it is, carry on tidying up, and make a note to ask someone what should really happen when we’ve discovered the correct abstractions. We may want to make removing a Shot an idempotent operation, so that we can damage multiple Klingons and only end up with a Shot being removed once.

There’s a Law of Demeter violation, in that the World knows how a Klingon copes with being hit. This unreasonably couples the implementations of these two classes, so let’s make it our responsibility to tell the Klingon that it was hit.

public class World {
  //...

  private Set<Klingon> klingonsWithin(Region influence) {
    //...
  }

  public void updateHits(){
    for (Shot shot : this.shots) {
      for (Klingon klingon : this.klingonsWithin(shot.getProximity())) {
        this.shots.remove(shot);
        this.explosions.add(new Explosion(shot));
        klingon.hit(shot);
      }
    }
  }
}

No, better idea! Let’s make the Shot hit the Klingon. Also, make the Shot responsible for knowing whether it disappeared (how many episodes of Star Trek are there where photon torpedoes get stuck in the hull of a ship?), and whether/how it explodes. Now we will be in a position to deal with the question we had earlier, because we can ask it in the domain language: “when a Shot might hit multiple Klingons, what happens?”. But I have a new question: does a Shot hit a Klingon, or does a Shot explode and the Explosion hit the Klingon? I hope this starship has a business analyst among its complement!

We end up with this World:

public class World {
  //...

  public void updateHits(){
    for (Shot shot : this.shots) {
      for (Klingon klingon : this.klingonsWithin(shot.getProximity())) {
        shot.hit(klingon);
      }
    }
  }
}

But didn’t I say that the shot understood the workings of its proximity fuze? Maybe it should search the World for nearby targets.

public class World {
  //...

  public void updateHits(){
    for (Shot shot : this.shots) {
      shot.hitNearbyTargets();
    }
  }
}

As described in the book, OOP is not about adding the word “class” to procedural code. It’s a different way of working, in which you think about the entities you need to model to solve your problem, and give them agency. Obviously the idea of “clean code” is subjective, so I leave it to you to decide whether the end state of this method is “cleaner” than the initial state. I’m happy with one fewer loop, no conditions, and no Demeter-breaking coupling. But I’m also happy that the “OO” example is now object-oriented. It’s now looking a lot less like enterprise software, and a lot more like Enterprise software.

Two books

A member of a mailing list I’m on recently asked: what two books should be on every engineer’s bookshelf? Here’s my answer.

Many software engineers, the ones described toward the end of Code Complete 2, would benefit most from Donald Knuth’s The Art of Computer Programming and Computers and Typesetting. It is truly astounding that one man has contributed so comprehensively to the art of variable-height monitor configurations.

If, to misquote Bill Hicks, “you’ve got yourself a reader”, then my picks are coloured by the fact that I’ve been trying to rehabilitate Object-Oriented Design for the last few years, by re-introducing a couple of concepts that got put aside over the recent decades:

  1. Object orientation; and
  2. Design.

With that in mind, my two recommendations are the early material from that field that I think shows the biggest divergence in thinking. Readers should be asking themselves “are these two authors really writing about the same topic?”, “where is the user of the software system in this book?”, “who are the users of the software system in this book?”, and “do I really need to choose one or other of these models, why not both or bits of both?”

  1. “Object-Oriented Programming: an evolutionary approach” by Brad Cox (there is another edition with Andrew Novobilski as a co-author). Cox’s model is the npm/CPAN model: programmers make objects (“software ICs”), describe their characteristics in a data sheet, and publish them in a catalogue. Integrators choose likely-looking objects from the catalogue and assemble an application out of them.

  2. “Object-Oriented Software Construction” by Bertrand Meyer. Meyer’s model is the “software engineering” model: work out what the system should do, partition that into “classes” based on where the data should naturally live, and design and build those classes. In designing the classes, pay particular attention to the expectations governing how they communicate: the ma as Alan Kay called the gaps between the objects.

Concurrent objects and SCOOP

Representing concurrency in an object-oriented system has been a long-standing problem. Encapsulating the concurrency primitives via objects and methods is easy enough, but doesn’t get us anywhere. We still end up composing our programs out of threads and mutexes and semaphores, which is still hard.

Prior Art

It’s worth skimming the things that I’ve written about here: I’ve put quite a lot of time into this concurrency problem and have written different models as my understanding changed.

Clearly, this is a broad problem. It’s one I’ve spent a lot of time on, and have a few satisfactory answers to if no definitive answer. I’m not the only one. Over at codeotaku they’ve concluded that Fibers are the right solution, though apparently on the basis of performance.

HPC programs are often based on concurrent execution through message passing, though common patterns keep it to a minimum: the batch processor starts all of the processes, each process finds its node number, node 0 divvies up the work to all of the nodes (a message send), then they each run through their part of the work on their own. Eventually they get their answer and send a message back to node 0, and when it has gathered all of the results everything is done. So really, the HPC people solve this problem by avoiding it.

You’re braining it wrong, Graham

Many of these designs try to solve for concurrency in quite a general way. Serial execution is a special case, where you only have one object or you don’t submit commands to the bus. The problem with this design approach, as described by Bertrand Meyer in his webinar on concurrent Object-Oriented Programming, is that serial execution is the only version we really understand. So designing for the general, and hard-to-understand, case means that generally we won’t understand what’s going on.

The reason he says this is so is that we’re better at understanding static relationships between things than the dynamic evolution of a system. As soon as you have mutexes and condition locks and so on, you are forced to understand the dynamic behaviour of the system (is this lock available? Is this condition met?). Worse: you have to understand it holistically (can anything that’s going on at the moment have changed this value?).

Enter SCOOP

Meyer’s proposal is that as serial programs are much easier to understand (solved, one might say, if one has read Dijkstra’s A Discipline of Programming) we should make our model as close to serial programming as possible. Anything that adds concurrency should be unsurprising, and not violate any expectations we had if we tried to understand our program as a sequential process.

He introduced SCOOP (Simple Concurrent Object-Oriented Programming) developed by the Concurrency Made Easy group at ETH Zürich and part of Eiffel. Some of the design decisions he presented:

  • a processor is an abstraction representing sequential execution
  • there is a many-to-one mapping of objects to processors (this means that an object’s execution is always serial, and that all objects are effectively mutexes)
  • where an object messages another on a different processor, commands will be asynchronous (but executed in order) and queries will be synchronous
  • processors are created dynamically and opportunistically (i.e. whenever you create an object in a “separate” and as-yet unpopulated domain)

An implementation of this concurrency model in Objective-C is really easy. A proxy object representing the domain separation intercepts messages, determines whether they are commands or queries and arranges for them to be run on the processor. It inspects the objects returned from methods, introducing proxies to tie them to the relevant processor. In this implementation a “processor” is a serial operation queue, but it could equivalently be a dedicated thread, a thread pulled from a pool, a dedicated CPU, or anything else that can run one thing at a time.

This implementation does not yield all of the stated benefits of SCOOP. Two in particular:

  1. The interaction of SCOOP with the Eiffel type system is such that while a local (to this processor) object can be referred to through a “separate” variable (i.e. one that potentially could be on a different processor), it is an error to try to use a “separate” object directly as if it were local. I do not see a way, in either Swift’s type system or ObjC’s, to maintain that property. It looks like this proposal, were it to cover generic or associated types, would address that deficiency.

  2. SCOOP turns Eiffel’s correctness preconditions into wait conditions. A serial program will fail if it tries to send a message without satisfying preconditions. When the message is sent to a “separate” object, this instead turns into a requirement to wait for the precondition to be true before execution.

Conclusions

Meyer is right: concurrent programming is difficult, because we are bad at considering all of the different combinations of states that a concurrent system can be in. A concurrent design can best be understood if it is constrained to be mostly like a serial one, and not require lots of scary non-local comprehension to understand the program’s behaviour. SCOOP is a really nice tool for realising such designs.

This is something I can help your team with! As you can see, I’ve spent actual years understanding and thinking about software concurrency, and while I’m not arrogant enough to claim I have solved it I can certainly provide a fresh perspective to your team’s architects and developers. Book an office hours appointment and let’s take a (free!) hour to look at your concurrency problems.

Microservices for the Desktop

In OOP the Easy Way, I make the argument that microservices are a rare instance of OOP done well:

Microservice adopters are able to implement different services in different technologies, to think about changes to a given service only in terms of how they satisfy the message contract, and to independently replace individual services without disrupting the whole system. This […] sounds a lot like OOP.

Microservices are an idea from service-oriented architecture (SOA) in which each application—each microservice—represents a distinct bounded context in the problem domain. If you’re a movie theatre complex, then selling tickets to people is a very different thing from showing movies in theatres, that are coupled loosely at the point that a ticket represents the right to a given seat in a given theatre at a given showing. So you might have a microservice that can tell people what showings there are at what times and where, and another microservice that can sell people tickets.

People who want to write scalable systems like microservices, because they can scale different parts of their application separately. Maybe each franchisee in the theatre chain needs one instance of one service, but another should scale as demand grows, sharing a central resource pool.

Never mind all of that. The real benefit of microservices is that they make boundary-crossing more obvious, maybe even more costly, and as a result developers think about where the boundaries should be. The “problem” with monolithic (single-process) applications was never, really, that the deployment cost too much: one corollary of scale is that you have more customers. It was that there was no real enforcement of separate parts of the problem domain. If you’ve got a thing over here that needs that data over there, it’s easy to just change its visibility modifier and grab it. Now this thing and that thing are coupled, whoops!

When this thing and that thing are in separate services, you’re going to have to expose a new endpoint to get that data out. That’s going to make it part of that thing’s public commitment: a slightly stronger signal that you’re going down a complex path.

It’s possible to take the microservices idea and use it in other contexts than “the backend”. In one Cocoa app I’m working on, I’ve taken the model (the representation in objects of the problem I’m solving) and put it into an XPC Plugin. XPC is a lot like old-style Distributed Objects or even CORBA or DCOM, with the exception that there are more safety checks, and everything is asynchronous. In my case, the model is in Objective-C in the plugin, and the application is in Swift in the host process.

“Everything is asynchronous” is a great reminder that the application and the model are communicating in an arm’s-reach fashion. My model is a program that represents the domain problem, as mentioned before. All it can do is react to events in the problem domain and represent the changes in that domain. My application is a reification of the Cocoa framework to expose a user interface. All it can do is draw stuff to the screen, and react to events in the user interface. The app and the model have to collaborate, because the stuff that gets drawn should be related to the problem, and the UI events should be related to desired changes in the domain. But they are restricted to collaborating over the published interface of the XPC service: a single protocol.

XPC was designed for factoring applications, separating the security contexts of different components and giving the host application the chance to stay alive when parts of the system fail. Those are valid and valuable benefits: the XPC service hosting the model only needs to do computation and allocate memory. Drawing (i.e. messaging the window server) is done elsewhere. So is saving and loading. And that helps enforce the contract, because if I ever find myself wanting to put drawing in the model I’m going to cross a service boundary, and I’m going to need to think long and hard about whether that is correct.

If you want to talk more about microservices, XPC services, and how they’re different or the same, and how I can help your team get the most out of them, you’re in luck! I’ve recently launched the Labrary—the intersection of the library and the laboratory—for exactly that purpose.

OOP the Easy Way: now 100% complete

Hello readers, part 3, the final part of the “OOP the Easy Way” journey, has now been published at Leanpub! Thanks for joining me along the way! As ever, corrections, questions, and comments are welcome (you can comment here if you like), and as ever, readers who buy the book now will receive free updates for the lifetime of the book. While there’s nothing new to add, this means that corrections and expansions will be free to all readers.

If you enjoy OOP the Easy Way or found it informative (or maybe even both), please recommend it to your friends, colleagues and followers. It’d be great if they could enjoy it, be informed by it, or both, too!

Book update: OOP the Easy Way

Obejct-Oriented Programming the Easy Way gets ever closer, as the first part (of three) is now substantively complete. If you have been holding off from buying the book, now would be a great opportunity to jump in, as a whole part of the book’s argument is now laid out. As ever, your feedback is welcome, and readers who buy now will get free updates throughout the development of the book.