Formal methods for the application programmer

[Andrew Wilcox]

I've been of the impression that using formal methods would be tedious and difficult, and yet would primarily be useful or important for complicated concurrent utilities such as transactional databases.

Thus, as an application developer, I'd use services such as a database which perhaps itself might make use of formal methods in its implementation, but formal methods wouldn't be relevant for me directly.

However, how do I know when I'm using a service such as a transactional database correctly?

For example, suppose I query the balance of my checking and savings accounts to find out how much money I have.  Naturally, if I were to do that query in a single transaction I'd get the right total, but if I were to incorrectly query the checking account and savings account balances in separate transactions I could get the wrong answer if a transfer happened to occur between queries.

1. start with $300 in checking and $700 in savings

2. query checking account balance: $300

3. transfer $100 from savings to checking

4. query savings account balance: $600

5. my calculated total: $900

This is obvious in a simple example, but in a more complicated situation I might not notice that I haven't set the boundaries of my transaction correctly.

How to find out if my code is correct?

I have the classic concurrent code dilemma of not being able to rely on testing (it's unlikely that a transfer will happen at just the wrong moment for the bug to be demonstrated), nor on inspection (each part of the code looks fine, it's only when one notices that the combination is incorrect that one can see that there's a problem).

Can formal methods help?  Would they be difficult?

To look at a concrete implementation, in JavaScript programming, promises have been becoming popular.

E.g.,

Promise.join(

  fetch_checking_balance(),

  fetch_savings_balance(),

  function (checking, savings) {

    report(checking + savings);

  }

);

asynchronously and simultaneously fetches the two balances (such as by making API calls), and, when both results are available, reports their sum.

A promise is said to be "fulfilled" when it has a value.  Thus fetch_checking_balance and fetch_savings_balance both return a promise, Promise.join waits until both have been fulfilled, and then calls the function in its last argument with the values of the promises.

(Promises can also be rejected with an error; and Promise.join will return a rejected promise if and as soon as any of its input promises reject, without waiting for the rest to complete.  I don't model rejected promises in this example though).

It looks like that waiting for a promise to be fulfilled can be easily and naturally modeled in Pluscal by using the await statement:

--algorithm Balance {

  variables

    \* checking account and savings account balances as stored in the database

    db_a = initialA;

    db_b = initialB;

    \* promises

    a_fulfilled = FALSE;     a_value = notset;

    b_fulfilled = FALSE;     b_value = notset;

    join_fulfilled = FALSE;  join_value = notset;

  define {

    total == 1000

    initialA == 300

    initialB == total - initialA

    transferAmount == 100

    notset == {}

  }

  

  process ( Transfer = "transfer" )

  {

    L1: db_a := db_a + transferAmount ||

        db_b := db_b - transferAmount;

  };

   

  process ( FetchA = "fetch_a" )

  {

    L2: a_fulfilled := TRUE || a_value := db_a;

  }

  

  process ( FetchB = "fetch_b" )

  {

    L3: b_fulfilled := TRUE || b_value := db_b;

  }

  

  process ( Join = "join" )

  {

    L4: await a_fulfilled /\ b_fulfilled;

        join_fulfilled := TRUE || join_value := << a_value, b_value >>;

  }

  

  process ( Report = "report" )

  {

    L5: await join_fulfilled;

        assert(LET a == join_value[1]

                   b == join_value[2]

               IN a + b = total)

  }

}

What's nice about this is that it's nearly a mechanical translation of the original promise code into Pluscal.

Running this in Pluscal immediately finds the cases where the assertion fails (when the calculated total is incorrect).

This is my first attempt so I don't know if such an approach would turn out to be practical for substantive programs.  I was pleasantly pleased however that it turned out to be so straightforward.

Andrew

[Leslie Lamport]

Hi Andrew,

You seem to be on the right path to learning what formal methods can
and cannot do.  You seem to be aware that they are crucial for
avoiding errors in concurrent systems.  Are they tedious and
difficult?  I think the Amazon experience described by Chris Newcombe
and his former colleagues show that TLA+/PlusCal itself isn't
difficult.  Building successful complex systems is difficult, and TLA+
helps make it a little easier.  Using any formal language is tedious;
it's easier to write things informally.  But a formal language is
necessary for tools, and I find writing in TLA+ or PlusCal to be a lot
less tedious than writing in a programming language because it's a
lot more expressive.  But of course, it takes a while to become
sufficiently fluent in a language before that can happen.

The one error I sense in your thinking is a false dichotomy between
formal methods and no methods.  It's important to understand what
you're building and, for non-trivial programming tasks, that requires
thinking above the code level.  Thinking above the code level means
describing/specifying/modeling what you're doing.  You should always
do that.  In some cases, you will want to write that
description/specification/model in a formal language.  The main reason
for doing that is so you can use tools to check it.  Occasionally,
what you're doing is so subtle and hard to understand that it's worth
using a formal language even if you're not using tools.  But even if
you don't use a formal language, it's important to write down that
description/spec/model--because that's the only way to be sure you
understand it.  Comments in the code are often a good place to write
it.  You might want to watch this video:

     https://www.youtube.com/watch?v=6QsTfL-uXd8

Good luck,

Leslie

[Andrew Wilcox]

     https://www.youtube.com/watch?v=6QsTfL-uXd8

Excellent introduction!  I recommend you include the link on your TLA+ page :)