SQL: Incorrect by Construction

SQL makes it easy to write incorrect code that looks right. Below is a textbook money-transfer procedure in TSQL. It looks reasonable, but it has three critical bugs. Can you spot them?

DECLARE @balance INT;

SET @balance = (  
    SELECT balance  
    FROM accounts
    WHERE owner = 'alice'
);

IF @balance >= 10  
BEGIN  
    UPDATE accounts  
    SET balance = balance - 10  
    WHERE owner = 'alice';  
  
    UPDATE accounts  
    SET balance = balance + 10  
    WHERE owner = 'bob';  
END

Atomicity

First of all, if this procedure gets aborted we might transfer money from Alice’s account without transferring anything to Bob—Alice won’t be happy about that, and we have destroyed money in the process. We want both transfers to succeed or neither. The fix is to wrap it in a transaction:

BEGIN TRANSACTION;

DECLARE @balance INT;

SET @balance = (  
    SELECT balance  
    FROM accounts
    WHERE owner = 'alice'
);

IF @balance >= 10  
BEGIN  
    UPDATE accounts  
    SET balance = balance - 10  
    WHERE owner = 'alice';  
  
    UPDATE accounts  
    SET balance = balance + 10  
    WHERE owner = 'bob';  
END

COMMIT TRANSACTION;

TOCTOU

Are we done yet? Not quite. Suppose Alice fires off two transfers to Bob in parallel, T1 and T2:

1. T1: Check the account balance
2. T2: Check the account balance
3. T1: Withdraw 10 from Alice’s account
4. T2: Withdraw 10 from Alice’s account
5. T1: Deposit 10 in Bob’s account
6. T2: Deposit 10 in Bob’s account

Note how we check the account balance in T2 before we have withdrawn the money in T1—this means that when it’s time to withdraw money in T2, Alice’s account balance might be too low. This is a Time-of-check to time-of-use bug: the precondition changes between when we check it and when we act on it.

The fix is to lock Alice’s row until the transaction completes. We can change the isolation level so locks are acquired automatically, or lock the row manually:

BEGIN TRANSACTION;

DECLARE @balance INT;

SET @balance = (  
    SELECT balance
    -- Called SELECT FOR UPDATE in some SQL dialects
    FROM accounts WITH (UPDLOCK)
    WHERE owner = 'alice'
);

IF @balance >= 10  
BEGIN  
    UPDATE accounts  
    SET balance = balance - 10  
    WHERE owner = 'alice';  
  
    UPDATE accounts  
    SET balance = balance + 10  
    WHERE owner = 'bob';  
END

COMMIT TRANSACTION;

The UPDLOCK hint takes a row-level lock on Alice’s account when the SELECT runs; other transactions block until ours commits.

Deadlocks

What if Alice and Bob both try to transfer money to each other at the same time? Let’s run through transactions T1 and T2 again:

1. T1: Acquire a lock on Alice’s account
2. T2: Acquire a lock on Bob’s account
3. T1: Check Alice’s account balance
4. T2: Check Bob’s account balance
5. T1: Withdraw 10 from Alice’s account
6. T2: Withdraw 10 from Bob’s account
7. T1: Can’t update Bob’s account because it’s locked by T2
8. T2: Can’t update Alice’s account because it’s locked by T1

T1 waits for T2’s lock on Bob; T2 waits for T1’s lock on Alice — a deadlock. The fix is to acquire all locks upfront:

BEGIN TRANSACTION;

DECLARE @balance INT;

SELECT owner
FROM accounts WITH (UPDLOCK)  
WHERE owner IN ('alice', 'bob');

SET @balance = (  
    SELECT balance
    FROM accounts
    WHERE owner = 'alice'
);

IF @balance >= 10  
BEGIN  
    UPDATE accounts  
    SET balance = balance - 10  
    WHERE owner = 'alice';  
  
    UPDATE accounts  
    SET balance = balance + 10  
    WHERE owner = 'bob';  
END

COMMIT TRANSACTION;

Conclusion

To summarize, we have added the following to our original example:

• Made updates atomic
• Prevented a TOCTOU bug
• Prevented a deadlock introduced by the locking strategy above ¹

In the process, the code became about 50% longer and much more difficult to read. Sure, you could argue that there are other, more idiomatic ways to fix this code², but the point still stands: What appeared to be perfectly reasonable code turned out to have several non-obvious bugs.

If you’re building a social media site, it might not be the end of the world if a user liked a post twice, but if a system fails to record that a patient received a dose of medicine it might have fatal consequences. For systems where correctness matters, we need better tools.

What I want is a query language that, like Rust, makes correctness the default:

• Make transactions atomic by default; if the user wants to save an intermediate “checkpoint” state they would have to say so explicitly.
• Locks should be explicit in the query rather than implicit in the isolation level.
• Use static analysis to detect deadlocks; this one is tricky and a subject of ongoing research. Deterministic database systems could be one possible solution.

This system will come with other trade-offs; for example, it might end up with lower throughput than modern SQL systems. But that’s fine-we still have SQL for use cases where correctness is less important.