• 2018-04-19

    Clean git histories and code review workflows

    A couple of recent tweets really resonated me.

    Aditya started an interesting conversation:

    I’ve always really liked having a “clean” history in the git logs of my projects. They look nicer! There’s a real joy to running git log (or even better, git log --graph --all!) on a project that’s maintained a beautiful log. There are a number of tangible benefits, too, which others have described well enough that I don’t need to repeat them here.

    More than that, though, for a long time I assumed that if you were using GitHub pull requests, there was One True Way to produce a clean history, echoed by Jesús:

    But recently, just like Aditya, I’ve had a change of heart! I realized that I was thinking about pull requests, and what they represent in terms of the final commit log I’m aiming for, in the wrong way. In this post I’ll describe the come-to-Aditya moment that made me appreciate squash-commits. And along the way I’ll have described two workflows that make it easy to keep a clean history: one that doesn’t use GitHub at all (and mimics how we did git-driven development before GitHub existed), and one that does.

  • 2018-03-27

    Introducing Network Error Logging

    Let’s say you’ve got a web site or REST service. You have clients that send requests to your server, which performs some interesting processing and sends responses back. The clients might be people using a browser, or native code in a mobile app making requests on behalf of the user, or something more exotic. But the overall picture is the same:

    request service flow

    How do you monitor this service — especially when that annoying cloudy bit in the middle is completely out of your control?

  • 2017-10-29

    Shared library versions

    Congratulations, you’ve written a software library! You hope that lots of people will find it useful, and will take it as a dependency when writing their own software. You know that at some point you’ll have to make changes to your library, either to add features or to fix bugs. Being a good maintainer, you want to be as diligent as possible in telling your users what to expect as you publish these changes. Will they need to change their code in response to the changes that you’ve made? Have you retired features that they depend on? Or are the changes “safe”, presumably requiring no updates on their part?

    The traditional approach is to encode all of this information into an easy-to-digest version number. Of course, nothing in this world is simple, so there are a number of different systems for encoding compatibility information into a version number. And surprisingly, if you’re writing a shared library for a compiled language like C or C++, there are (at least!) two different versioning systems that you’ll need to learn. In this post, we’re going to look at these different systems, how they relate to each other, and how to actually apply these version numbers to your library using a couple of common build tools.

  • 2017-08-10

    Obligations

    Introduction

    Programming languages have a lot of interesting ways to think about what you’re allowed to do, and not allowed to do. In a statically typed language, your compiler will yell at you if you try to do something that’s not allowed, and a lot of interesting PL research involves teaching your language and compiler to disallow things in increasingly sophisticated ways.

    This is not limited to statically typed languages. In a dynamically typed language, your interpreter is just as invested in disallowing certain behaviors. It’s just that the enforcement happens while your program is running!

    Someone with a theoretical background might quibble with my choice of the word “disallow”. They might prefer that I say that certain operations in your programming language are “invalid”. In the world of mathematics, it’s usually not the case that some little gremlin is actively preventing these operations from occurring; instead, it’s that the invalid operations don’t even exist as possibilities!

    But regardless what language you’re programming in, and regardless of whether you think in terms of permissions or possibilities, the act of programming is to consider all of these possible operations, and choose which ones you want to use to accomplish your goal. At any given time, there are many possible operations, and you have the control to decide which ones to use!

    In this series of posts I want to look at the flip side of this, and talk about requirements or obligations. What mechanisms do programming languages have to force you to perform some operation, or to ensure that some operation is performed even if you don’t actively choose to do it yourself?

    At the end of this series, I hope to convince you that obligations are just as important as possibilities, and that there are interesting complex behaviors that are easier to think about and work with if we use programming languages that can talk about obligations directly.

  • 2017-01-17

    HST

    Lazy processes

    1. Load in a description of the \(Spec\) and \(Impl\) processes, transforming them each into a labeled transition system (LTS).

    As mentioned in the previous post, we’re going to rely on the labeled transition system defined by CSP’s operational semantics to represent processes in our refinement checker. An LTS is just a directed graph, with nodes representing processes and subprocesses, and edges representing events. In this post, we’ll look at LTSes in a bit more detail, and at how best to represent them in code.

  • 2016-11-17

    HST

    Semantic methods

    Since CSP is a formal method, it’s not surprising that Roscoe spends a large part of his textbook talking about how to use rigorous mathematics to talk about processes. He actually goes one step (er, two?) further and defines three different ways to do so:

    • The denotational semantics defines (mathematically, using sets and sequences) what the behavior of a process is. Each CSP operator comes with a rule for how to calculate a process’s behavior recursively — that is, in terms of the behavior of its operands. (So for example, the “external choice” rule tells you how to define the behavior of \(P \mathrel{\Box} Q\) in terms of the behavior of \(P\) and \(Q\).)

    • The algebraic semantics tell you to not worry about what a process “means” or what it “does”. Instead, it provides a list of rewrite rules that let you change what the definition of a process looks like without changing its behavior.

    • The operational semantics say that a process is nothing more than a state machine, with nodes representing processes (and subprocesses) and edges representing the events that allow you to transition between them. We can learn anything important about a process just by interpreting or analyzing this state machine.

  • 2016-11-17

    HST

    Refinement overview

    Our goal is to learn about CSP refinement by implementing a refinement checker. So a good first step is to make sure we’re all on the same page about what refinement is, and then to step through the refinement algorithm that we mean to implement. (If nothing else, that will help make sure I don’t go off on too many tangents while implementing it!)

    I’ve mentioned refinement elsewhere on this blog a few times (for instance, here). The basic idea is that in CSP, you use the same process language to describe the system you’re designing or investigating, as well as the properties that you would like that system to have. (This is unlike most other formal methods, where you have separate languages for the system and the properties.) In CSP, the system’s process is typically called \(Impl\) (for implementation), and the property description process is typically called \(Spec\) (for specification).

    CSP then defines several semantic models that provide rigorous mathematical definitions of what a process’s behavior is. You perform a refinement check within the context of a particular semantic model. A successful refinement check tells you that the property defined by \(Spec\) “holds” — specifically, that all of the behaviors of \(Impl\) are also allowed behaviors of \(Spec\). A failed refinement check gives you a counterexample — that is, a specific behavior of \(Impl\) that was disallowed by \(Spec\).

    The three most common semantic models are traces, failures, and failures-divergences. We’ll go into more detail about the mathematics behind these semantic models in later posts; for now, the 10,000-foot overview is that:

  • 2016-11-16

    HST

    Introduction

    It seems like this blog is basically turning into “all things CSP”! As part of that trend, I’ve started implementing a new CSP refinement checker called HST. Why do this when there’s a perfectly good refinement checker in FDR? Well, I want to learn more about how FDR’s refinement algorithm works. The algorithm is documented in Bill Roscoe’s textbook (and a series of follow-on papers), and working through those descriptions gives you a good bit of insight into how refinenment really works. But I often find it easier to learn a complex topic by implementing it (or at least, by looking at the code of an implementation). Hence HST! In this new series of blog posts, I’m going to walk through the CSP refinement algorithm in more detail than is presented in the academic literature, by implementing it (and describing that implementation) along the way.

    I should emphasize that this is not meant to be a replacement for FDR! FDR is a very good piece of software, and if you’re writing any CSP specs in anger, you probably want FDR at your disposal. HST is meant to be more of an educational exercise. If people find it more generally useful than that, that’s great! But it’s not what I’m aiming for.

    (And as for the name, “HST” does not stand for “Harry S. Truman”, just like “FDR” does not stand for “Franklin Delano Roosevelt”.)

  • 2016-09-07

    Concurrency models in CSP

    Read Atomic: Internal consistency

    We’ll start by looking at the weakest concurrency model covered in the paper, Read Atomic. In fact, to keep things really simple to start with, we’re only going to look at one of Read Atomic’s two axioms: internal consistency. (We’ll look at external consistency in the next post.)

    A transaction is internally consistent if it “reads its own writes”. This is the simplest axiom covered in the paper, since it expresses a property that’s strictly local to each transaction; we don’t have to consider the behavior of any other transaction when defining what it means for a transaction to be internally consistent.

  • 2016-08-03

    Concurrency models in CSP

    Preliminaries

    Before diving into the details of our first concurrency model, it will be helpful to give an overview of how we’re going to use CSP in these posts.

    At the highest level, a CSP specification consists of a set of processes, which use events to describe their behavior. We use a process to represent any vantage point that lets us talk about which events occur and in which order. Each entity in our system is a process (which might be defined using subprocesses to describe each of its components or parts). We also use processes to describe how two or more entities interact with each other, and to describe any global properties of the entire system. And lastly, because CSP verification is based on “refinement”, we also use processes to define the properties that we hope our system exhibits.