Archive for the ‘qed’ Category

Speaking at the North Dallas .NET Users Group

Sunday, July 4th, 2010

I’ll be speaking at NDDNUG on Wednesday about the CAP Theorem and its implications. Here’s a preview of what you can expect:

I’ll be posting slides and source code at qedcode.com. Hope to see you there.

Topic specific sites

Saturday, October 10th, 2009

I now have three sites for topic-specific content.

I have seeded these sites with articles from Adventures in Software. But from now on, articles specific to those topics will go on those sites. Please subscribe to those RSS feeds as well as this one.

A provable Socket API

Thursday, October 8th, 2009

Two weeks ago, I assigned homework. Rewrite the .NET Socket API so that you can prove the following assertions:

  • You cannot use a Socket returned from Accept to accept any additional connections from the connection queue.
  • You cannot call Accept, Bind, Connect, Listen, Receive, or Send if the socket has been closed.
  • You must call Bind before you can call the Listen method.
  • You must call Listen before calling Accept.
  • Connect(string host, int port) can only be called if addressFamily is either InterNetwork or InterNetworkV6.
  • Connect cannot be called if Listen has been called.
  • You have to either call Connect or Accept before Sending and Receiving data.
  • If the socket has been previously disconnected, then you cannot use Connect to restore the connection.

These assertions are prominently listed in the MSDN documentation. Why not roll them into the API itself? Let the compiler prove that we are using sockets correctly.

Last week, I gave you a hint. I moved the Send and Receive methods out to a different class so that we can prove that you've called Accept or Connect prior to Send or Receive. Both Accept and Connect became factory methods. You must call the factory before you get the object, and you must get the object before you call its methods. Q.E.D.

Let's start from there and prove the rest of the assertions.

Starting point

  • You have to either call Connect or Accept before Sending and Receiving data.
public class ConnectedSocket
{
    public int Receive(byte[] buffer);
    public int Send(byte[] buffer);
}

public class Socket : IDisposable
{
    public Socket(SocketInformation socketInformation);
    public Socket(AddressFamily addressFamily, SocketType socketType, ProtocolType protocolType);

    public ConnectedSocket Accept();
    public void Bind(EndPoint localEP);
    public ConnectedSocket Connect(EndPoint remoteEP);
    public ConnectedSocket Connect(string host, int port);
    public void Dispose();
    public void Listen(int backlog);
}

Looking through the list of assertions, we find that this one is already taken care of by the first change:

  • You cannot use a Socket returned from Accept to accept any additional connections from the connection queue.

The ConnectedSocket class doesn't have an Accept method, so you can't call it. Q.E.D.

Other prerequisites
There are three other prerequisite assertions that we can prove in exactly the same way:

  • You must call Bind before you can call the Listen method.
  • You must call Listen before calling Accept.
  • Connect cannot be called if Listen has been called.
public class Socket : IDisposable
{
    public Socket(SocketInformation socketInformation);
    public Socket(AddressFamily addressFamily, SocketType socketType, ProtocolType protocolType);

    public BoundSocket Bind(EndPoint localEP);
    public ConnectedSocket Connect(EndPoint remoteEP);
    public ConnectedSocket Connect(string host, int port);
    public void Dispose();
}

public class BoundSocket
{
    public ListeningSocket Listen(int backlog);
    public ConnectedSocket Connect(EndPoint remoteEP);
    public ConnectedSocket Connect(string host, int port);
}

public class ListeningSocket
{
    public ConnectedSocket Accept();
}

Bind becomes a factory for the class that gives you Listen. Bind does not take away your ability to call Connect. Listen does.

Factory and product
Factories are great prerequisites. Now that it is becoming more obvious that we are using that pattern, let's rename Socket and move IDisposable to the product.

public class SocketFactory
{
    public SocketFactory(SocketInformation socketInformation);
    public SocketFactory(AddressFamily addressFamily, SocketType socketType, ProtocolType protocolType);

    public BoundSocket Bind(EndPoint localEP);
    public ConnectedSocket Connect(EndPoint remoteEP);
    public ConnectedSocket Connect(string host, int port);
}

public class ConnectedSocket : IDisposable
{
    public int Receive(byte[] buffer);
    public int Send(byte[] buffer);
    public void Dispose();
}

The ConnectedSocket is the ultimate product. That's the socket that needs to be closed. And what do you know, this change proves another of our assertions:

  • If the socket has been previously disconnected, then you cannot use Connect to restore the connection.

It is impossible to call Connect on a socket that has been disposed, since they aren't the same object anymore.

Dispose once
Now that the Dispose method is where it belongs, let's focus on the assertion most concerned with its use:

  • You cannot call Accept, Bind, Connect, Listen, Receive, or Send if the socket has been closed.

Accept, Bind, Connect, and Listen have already been taken care of, since they have become factory methods. To handle Send and Receive, we turn every ConnectedSocket factory into a callback:

public class ConnectedSocket
{
    public int Receive(byte[] buffer);
    public int Send(byte[] buffer);
}

public void Connect(string host, int port, Action<ConnectedSocket> action);

We have taken away the capability of disposing a socket. The factory does it on the consumer's behalf. Since there is no way for the consumer to call Dispose, and since the callback returns before Dispose is called, there is no way to call Send or Receive after Dispose. Q.E.D.

Specialized factory
Which leaves us with one final assertion:

  • Connect(string host, int port) can only be called if addressFamily is either InterNetwork or InterNetworkV6.

Again, we want to move the restricted method into its own special class. But now, we want to enforce that certain values are provided, not that certain methods are called. We'll limit this by creating our own smaller enumeration.

public class IPSocketFactory : SocketFactory
{
    public enum Version { V4, V6 }
    public IPSocketFactory(Version version, SocketType socketType, ProtocolType protocolType)
        : base(
            version == Version.V4 ? AddressFamily.InterNetwork : AddressFamily.InterNetworkV6,
            socketType,
            protocolType) { }

    public void Connect(string host, int port, Action<ConnectedSocket> action);
}

If you want to call the Connect overload with two parameters, you have to use the limited enumeration to get the right factory. I didn't mess with the overloaded constructor, because it complicates things.

One slight wrinkle. In a previous change we created a copy of the Connect method, since it can be called after Bind(). So we make the same change there:

public class IPBoundSocket : BoundSocket
{
    public void Connect(string host, int port, Action<ConnectedSocket> action);
}

public class IPSocketFactory : SocketFactory
{
    public enum Version { V4, V6 }
    public IPSocketFactory(Version version, SocketType socketType, ProtocolType protocolType)
        : base(
            version == Version.V4 ? AddressFamily.InterNetwork : AddressFamily.InterNetworkV6,
            socketType,
            protocolType) { }

    public IPBoundSocket Bind(EndPoint localEP);
    public void Connect(string host, int port, Action<ConnectedSocket> action);
}

The only way to get an IPBoundSocket is to use the IPSocketFactory. Therefore, you must have selected one of the Internet protocols. By the way, this is taking advantage of a little-used feature of C# called covarience. This is the one part of the proof that might not work in other languages.

So there you have it. A provably correct Socket API. There is no way to use it incorrectly. The compiler enforces all of the assertions that we would otherwise have to read the documentation to discover.

Hint on socket homework

Thursday, October 1st, 2009

Your homework is extended for another week, but let me give you a hint what I'm looking for. The problem was to Fix the Socket API. Rewrite the .NET Socket interface so that the assertions made in the MSDN documentation can be proven.

To give you an example of what I'm looking for, take the following assertion:

  • You have to either call Connect or Accept before Sending and Receiving data.

This is a prerequisite assertion. We must first call Connect or Accept, then we can call Send or Receive. To prove this assertion, I'll use factory methods. Here's the original Socket class:

public class Socket : IDisposable
{
    public Socket(SocketInformation socketInformation);
    public Socket(AddressFamily addressFamily, SocketType socketType, ProtocolType protocolType);

    public Socket Accept();
    public void Bind(EndPoint localEP);
    public void Connect(EndPoint remoteEP);
    public void Connect(string host, int port);
    public void Dispose();
    public void Listen(int backlog);
    public int Receive(byte[] buffer);
    public int Send(byte[] buffer);
}

Move the Send and Receive methods out of this class. We cannot call them yet. Move them into a new class called ConnectedSocket.

public class ConnectedSocket
{
    public int Receive(byte[] buffer);
    public int Send(byte[] buffer);
}

To prove that we have to call Connect or Accept before any of the ConnectedSocket methods, we make Connect and Accept factory methods:

public class Socket : IDisposable
{
    public Socket(SocketInformation socketInformation);
    public Socket(AddressFamily addressFamily, SocketType socketType, ProtocolType protocolType);

    public ConnectedSocket Accept();
    public void Bind(EndPoint localEP);
    public ConnectedSocket Connect(EndPoint remoteEP);
    public ConnectedSocket Connect(string host, int port);
    public void Dispose();
    public void Listen(int backlog);
}

This API proves one of the assertions in the MSDN documentation. Try the others on your own. Answers will be posted next week.

Relaxed locking on thread-safe cache

Friday, September 18th, 2009

In a prior post, I showed how callbacks can be used to prove prerequisites and thread-safety. The example was a cache. But the solution left the cache too constraining. While it was correct, it was too tightly locked. All users of the class will line up behind one another, whether they are after the same data or not.

To resolve this problem, let's move the lock. Instead of locking on the cache while fetching the value, let's lock on the key. Two clients accessing the cache with the same key will line up, but clients with different keys will not.

But we can't lock on the key itself. We need to lock on something with identity. The identity of the key is not important. A client can create a new instance of the key having the same value, and that should qualify as the same key. So we have to look elsewhere.

Fortunately, the value of the key is used to find an object in the dictionary. That object does have identity. So we move the lock there.

public class CachedObject<TValue>
{
    private TValue _value;
    private bool _fetched = false;
    public DateTime DateCached { get; private set; }

    public CachedObject(DateTime dateCached)
    {
        DateCached = dateCached;
    }

    public TValue Value
    {
        get { return _value; }
        set { _value = value; _fetched = true; }
    }

    public bool Fetched
    {
        get { return _fetched; }
    }
}

public class Cache<TKey, TValue>
{
    private TimeSpan _expiry;
    private Dictionary<TKey, CachedObject<TValue>> _store =
        new Dictionary<TKey, CachedObject<TValue>>();

    public Cache(TimeSpan expiry)
    {
        _expiry = expiry;
    }

    public TValue Get(TKey key, Func<TKey, TValue> fetch)
    {
        CachedObject<TValue> found;

        lock (_store)
        {
            // If the object is not in the cache, or it is expired,
            // fetch it and add it to the cache.
            DateTime now = DateTime.Now;
            if (_store.TryGetValue(key, out found) &&
                found.DateCached + _expiry < now)
            {
                return found.Value;
            }

            found = new CachedObject<TValue>(now);
            _store.Add(key, found);
        }

        lock (found)
        {
            if (!found.Fetched)
                found.Value = fetch(key);
            return found.Value;
        }
    }
}

The Get method locks first on the cache. This protects the data structure, and ensures that we get just one instance of CachedObject. Once it has that, it locks on the found CachedObject so that clients after the same key line up.

Inside the lock, it checks to see whether the value has already been fetched. If not, this thread is the first in line, so it fetches the value. But if it has already been fetched, then the thread was not the first in line and can just use the fetched object.

The above is not a formal proof, and has many logical holes. Hopefully we'll have time to shore it up, and possibly find bugs in the code along the way. This is the kind of code that definitely needs to be proven. Sure, unit testing can give us some confidence, but no amount of unit testing can verify that this code is completely thread safe.

Thread safety through callbacks

Wednesday, September 16th, 2009

While callbacks are good at proving prerequisites, they are also good at proving thread safety. Take, for example, this cache:

public class CachedObject<TValue>
{
    public TValue Value { get; private set; }
    public DateTime DateCached { get; private set; }

    public CachedObject(TValue value, DateTime dateCached)
    {
        Value = value;
        DateCached = dateCached;
    }
}

public class Cache<TKey, TValue>
{
    private TimeSpan _expiry;
    private Dictionary<TKey, CachedObject<TValue>> _store =
        new Dictionary<TKey, CachedObject<TValue>>();

    public Cache(TimeSpan expiry)
    {
        _expiry = expiry;
    }

    public TValue Get(TKey key)
    {
        CachedObject<TValue> found;

        // If the object is in the cache, check the date.
        if (_store.TryGetValue(key, out found) &&
            found.DateCached + _expiry < DateTime.Now)
        {
            return found.Value;
        }
        else
        {
            return default(TValue);
        }
    }

    public void Put(TKey key, TValue value)
    {
        _store.Add(key, new CachedObject<TValue>(value, DateTime.Now));
    }
}

The caller has to use it properly for it to work. They have to call Get before Put (prerequisite), and they have to synchronize around the two calls. If they don't, they run the risk of creating a race condition.

A race condition occurs when the outcome of an operation depends upon other operations happening in parallel. If one thread gets finished first, there is one result. If another thread finishes first, there is another. In this case, two threads could try to Get the same value. Finding none, they can both race to fetch the value and put it in the cache.

To prove that a race condition cannot occur, we can use a callback.

public class Cache<TKey, TValue>
{
    private TimeSpan _expiry;
    private Dictionary<TKey, CachedObject<TValue>> _store =
        new Dictionary<TKey, CachedObject<TValue>>();

    public Cache(TimeSpan expiry)
    {
        _expiry = expiry;
    }

    public TValue Get(TKey key, Func<TKey, TValue> fetch)
    {
        lock (_store)
        {
            CachedObject<TValue> found;

            // If the object is not in the cache, or it is expired,
            // fetch it and add it to the cache.
            DateTime now = DateTime.Now;
            if (!_store.TryGetValue(key, out found) ||
                found.DateCached + _expiry >= now)
            {
                found = new CachedObject<TValue>(fetch(key), now);
               _store.Add(key, found);
            }
            return found.Value;
        }
    }
}

This version of the cache takes a callback to fetch the value if it is not found. Synchronization is now built into the Get method. The caller doesn't need to synchronize around it. More importantly, we can prove the correctness of the code without seeing the caller. There is no way to get it wrong.

This cache still has problems. The lock is to broad. In preventing a race condition on two thread getting the same value, we've inadvertently blocked two threads getting different values. We'll fix that next.

Fixing an unhelpful API

Tuesday, September 15th, 2009

I started Q.E.D. Hour at work to discuss ways that we can use mathematical proof to have more confidence in our code. In last week's session, we walked through some improvements to a particular piece of code. Here is how it started:

public void DoWorkWithOrderService()
{
    using (ITransaction currentTransaction = new AcidTransaction(_container))
    {
        OrderService.Transaction = currentTransaction;
        OrderService.DoWork();
        currentTransaction.Commit();
    }
}

It is only possible to prove the correctness of this code based on the caller (seen here), and not the order service itself. If the caller forgets to initialize the transaction property, if the caller forgets to create the transaction in a using statement, or if the caller forgets to create a new instance per thread, then bad things can happen.

Unhelpful_API The order service is an unhelpful API. When you approach it, you have to use caution. If you use it in the wrong way, bad things will happen. If you're lucky, it will throw an exception. If you are unlucky, you won't catch errors until you release to production.

An unhelpful API must be approached with fear.

Parameters are prerequisites
The first step in improving this unhelpful API is to ensure that a transaction exists before a service method is called. We can do this by turning the property into a parameter.

Before:

public class Service : IService
{
    public ITransaction Transaction
    {
        set;
        get;
    }

    public void DoWork() { }
}

After:

public class ServiceFactory : IServiceFactory
{
    public IService CreateService(ITransaction transaction)
    {
        return new Service(transaction);
    }
}

public class Service : IService
{
    private ITransaction _transaction;

    public Service(ITransaction transaction)
    {
        _transaction = transaction;
    }

    public void DoWork() { }
}

You cannot get a service from the factory without providing a transaction. Therefore, you cannot make any service calls before providing a transaction. Q.E.D.

Callbacks are prerequisites
We have proven that a transaction is provided before a service method is called, but we haven't yet proven that the transaction gets disposed. We can take one more step toward making this a helpful, provable API using a callback.

public class ServiceFactory : IServiceFactory
{
    private ITransactionFactory _transactionFactory;

    public void CallService(Action<IService> action)
    {
        using (ITransaction transaction =
            _transactionFactory.CreateTransaction())
        {
            action(new Service(transaction));
        }
    }
}

A transaction factory is injected into the service factory (via constructor not shown here), and that is used to create a transaction as needed. That creation happens within a using statement in the service factory, not in the calling code. There is no way for the caller to forget to do this. Thus we have proven that the transaction gets disposed.

In these two steps, we have transformed an unhelpful API into a helpful one. The unhelpful API offered many options, most of them wrong. The helpful API offers only the options that are correct. It guides the caller in its proper use. It cannot be used incorrectly.

An unhelpful API cannot be proven. It must be approached with fear. A helpful API can be proven. It can be approached with confidence.

Proof based on imperative programming

Monday, September 14th, 2009

Our Q.E.D. homework for last week was to prove some code to be correct. In particular, prove that:

  • The service has a transaction when it is called.
  • The transaction is disposed.
  • The code is thread safe.

The code in question was:

public Order GetOrder(int orderId)
{
   return InvokeGetOrder(() => OrderServiceProvider.GetOrderWithItems(orderId));
}

public Order InvokeGetOrder(Func<Order> function)
{
    Order order;
    using (IBusinessTransactionContext currentBusinessTransactionContext =
        new AcidBusinessTransactionContext(_container, false))
    {
        OrderServiceProvider.BusinessTransactionContext =
            currentBusinessTransactionContext;

        order = function();
        OrderServiceProvider.BusinessTransactionContext.Commit();
    }

    return order;
}

The proof of the first two points is pretty straight forward. Because the transaction is assigned prior to calling the service function, we know the service function has a transaction. And because the transaction is created in a using statement, we know that it will be disposed.

The third point is harder to prove. If two threads call GetOrder on the same object, they will both try to assign a transaction to the same OrderServiceProvider. We have to prove that this won't happen. For that, we look at the Castle configuration:

<component
    id="...OrderService"
    service="...OrderService, ..."
    type="...OrderService, ..."
    lifestyle="transient>
        <parameters>
            <orderRepository>
                ${...OrderRepository}
            </orderRepository>
        </parameters>
</component>

Because the OrderService is declared to be transient, we are guaranteed to get a new instance each time the component is resolved. Each web request resolves the service, so we know that each web request gets a unique object. The request is thread safe. Q.E.D.

Perils of imperative proofs
While these proofs are correct, there is a significant problem. We proved correctness based on the code that calls OrderService, not based on OrderService itself. In fact, there is nothing about the OrderService API that compels the caller to use it correctly.

For example, the service requires that we set the BusinessTransactionContext property before we call a method. If we forget one little assignment statement, then the service does not have a transaction. This problem can be caught no earlier than integration testing.

If, on the other hand, we forget to create our transaction in a using statement, we have a more subtle problem. We may see that database connections leak over time. Or we may see blocking because failed transactions remain open instead of being rolled back. This problem won't be caught in integration testing, and may be very difficult to diagnose when it finally is identified.

And what if we forget to configure our components to be transient? The only time this causes a measurable problem is when we have concurrency greater than 1. This doesn't happen during a typical integration test. Nor does this usually happen during manual testing. The first time a web application sees concurrency is usually during stress testing, or maybe even production.

This lead into a discussion of prerequisites. There are ways that we can rewrite the OrderService API so that it cannot be used incorrectly. Some examples are to require a parameter and to use the constructor. We'll apply these techniques to the OrderService in the next post.

My wish for C#: class parameters

Friday, September 11th, 2009

How C# works today:

public class Order
{
    private Customer _customer;

    public Order(Customer customer)
    {
        _customer = customer;
    }

    public Customer Customer
    {
        get { return _customer; }
    }

    public void Fulfill()
    {
        Package.ShipTo(_customer.ShippingAddress);
    }
}

How I wish it worked:

public class Order(Customer _customer)
{
    public Customer Customer
    {
        get { return _customer; }
    }

    public void Fulfill()
    {
        Package.ShipTo(_customer.ShippingAddress);
    }
}

Advantages:

  • Class parameters would be immutable.
  • Classes could only have one constructor.
  • Constructors could not have side effects.
  • Constructors could not throw exceptions.
  • Class parameters would only have to be declared once instead of 3 times (counting the assignment).

Anonymous delegates vs. lambdas

Thursday, September 10th, 2009

An interesting question came up during last week's Q.E.D. discussion on closure. Why are there two language features in C# that do the same thing?

Lambdas:

public Order GetOrder(string orderId)
{
    return GetOrderRepository()
        .GetSatisfying(o => o.OrderId == orderId)
        .Query()
        .FirstOrDefault();
}

Anonymous delegates:

public Order GetOrder(string orderId)
{
    return GetOrderRepository()
        .GetSatisfying(delegate(Order o)
            { return o.OrderId == orderId; })
        .Query()
        .FirstOrDefault();
}

Do you see the difference? Let me give you a clue. Here's another way to write the anonymous delegate:

public Order GetOrder(string orderId)
{
    return GetOrderRepository()
        .GetSatisfying(o =>
           { return o.OrderId == orderId; })
        .Query()
        .FirstOrDefault();
}

Even though this syntax uses the lambda operator "=>", it still behaves more like an anonymous delegate. The important difference is not the "=>" or the "delegate", its the "return" and the semicolon.

A lambda contains an expression. An anonymous delegate contains statements. Sure, that could be a single return statement, but it doesn't have to be.

It should be stated that only the first block of code compiles in this instance. That's because GetSatisfying takes "Expression<Func<Order, bool>>", and not just "Func<Order, bool>". A function is just a block of code that you can call which happens to return a value. An expression, on the other hand, exists only to produce that value.

Lambdas are expressions. Anonymous delegates are functions.