Hardware/software verification enters the atomic age: Part 1

George Harper

March 23, 2008

George Harper

While the 1940s and 1950s saw the dawn of the nuclear age for power and weaponry, a half a century later we're just now entering an atomic age of a different sort. Having little to do with radioactivity, this atomic age is about software and hardware design, specifically using atomic transactions, by far the most powerful technique for managing one of our most tricky problems, concurrency.

Even if you haven't heard of atomic transactions before, they're likely to have an impact on your future work, whether you design embedded software, architect systems, perform verification, or design hardware. Atomic transactions are not a new technology, but the increasing complexity and amount of concurrency in systems is pressing their emergence in all of these areas.

So, just what are atomic transactions? And, how are they already manifesting themselves in embedded systems software, processor, and hardware design? After introducing atomic transactions and ways in which they're revealing themselves, this article will take a special look at their implications to verification.

Atomic Transactions 101
If you are familiar with database transactions, you've probably already been exposed to atomic transactions. When processing multiple, simultaneous transactions, databases use atomic transactions to maintain consistency. Imagine a couple who share a bank account and simultaneously make two withdrawals of $100 from separate ATM machines across town (Figure 1). Several steps are involved in each withdrawal: A) checking the balance; B) providing the money and calculating the new balance, and; C) updating the balance with the new amount.

Now imagine that each step were independent (1A, 1B, and 1C for one of the couple and 2A, 2B and 2C for the other) and performed in the following order: 1A, 2A, 1B, 2B, 1C, 2C. What would happen? Both would receive $100, but the bank account would only be debited a total of $100, instead of $200.

View the full-size image

Databases use atomic transactions to prevent this inconsistency from occurring and ensure that steps A, B, and C happen together and indivisibly for each withdrawal transaction. Atomic transactions ensure that the two withdrawals are performed in one of two orders: 1A, 1B, 1C, 2A, 2B, 2C or 2A, 2B, 2C, 1A, 1B, 1C.

Atomic transactions have the same properties that we saw in the bank ATM example. These transactions are atomic, which means that they are indivisible and all-or-nothing. Atomicity ensures that multiple, related operations occur indivisibly, as though they're happening in isolation and without having to be concerned about other system activities.

And, atomicity ensures that multiple, related operations are all-or-nothing--all of the operations in a transaction are completed or none of them are completed. These properties ensure a consistent state relative to all other transactions in the system.

Many high-level specification languages for concurrent systems express concurrent behavior as a collection of rewrite rules, where each rule has a guard (a Boolean predicate on the current state) and an action or set of actions that transform the state of the system.