Embedded Systems Design Europe - April 2008 - (Page 34)

veriﬁcation 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. 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 speciﬁcation 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. The active rules, where the guards are true, can be applied in parallel, but each rule operates as an atomic transac34 tion – each rule observes and ensures a consistent state relative to all other rules in the system. This atomicity model is popular because it enables concurrent behavioral descriptions of the highest abstraction and simpliﬁes the reasoning around correctness. TRS EXPRESSES ATOMICITY One example of a high-level speciﬁcation language using this computational model is the term rewriting system (TRS). TRSs offer a convenient way to describe parallel and asynchronous systems and prove an implementation’s correctness with respect to a speciﬁcation. TRS descriptions, augmented with proper information about the system building blocks, also hold the promise of high-level synthesis. High-level architectural descriptions that are both automatically synthesizable and veriﬁable would permit architectural exploration at a fraction of the time and cost required by current commercial tools. A TRS is deﬁned as a tuple (S, R, S ), where S is a set of terms, R is a set of rewriting rules, and S is a set of initial terms. The state of a system is represented as a TRS term, while the state transitions are represented as TRS rules. The general structure of rewriting rules is: 0 0 (1) where s and s are terms, and p is a predicate. We can use a rule to rewrite a term if the rule’s left-hand-side pattern matches the term or one of its subterms, and the corresponding predicate is true. The new term is generated in accordance with the rule’s right-hand side. If several rules apply, then any one of them can be applied. If no rule applies, the term cannot be rewritten any further. In practice, we often use abstract data 1 2 APRIL 2008 | embedded systems design europe | www.embedded.com/europe 033-034-035-036.indd 34 8/04/08 12:35:36 http://www.embedded.com/europe

Table of Contents Feed for the Digital Edition of Embedded Systems Design Europe - April 2008

Embedded Systems Design Europe - April 2008 Contents Chip Industry Confronts 'Software' Gap Wind River's VxWorks OS Part of the nEUROn UCAV Demonstrator iSuppli Cuts Electronic Equipment Forecast Study Says GigE Vision Not Mature Chip Aids Wireless Health Monitoring Kontron Reports Strong Financial Growth Xilinx Completes Virtex-5 Line-Up French Project Builds Open Platform Home Automation Group Uses Enocean Radio Layer MIPs Adds Multi-Core Option to Portfolio Cover Feature: Next Gen Programmable Chips: Why Can't Hardware Be More Like Software? Improving Productivity & Quality With Domain-Specific Modeling Efficient CRC Calculation With Minimal Memory Footprint Do-It-Yourself Linux Embedded Development Tools Hardware/Software Verification Enters the Atomic Age New Products Advertising Contacts

Embedded Systems Design Europe - April 2008

For optimal viewing of this digital publication, please enable JavaScript and then refresh the page. If you would like to try to load the digital publication without using Flash Player detection, please click here.