Embedded Systems Design - March 2008 - (Page 28)

0308esd.p27to31 2/13/08 7:53 PM Page 28 feature A common instance of the use of atomic transactions is in databases, such as those used in ATM machine applications. The example here shows simultaneous withdrawals from one account. 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, S0), where S is a set of terms, R is a set of rewriting rules, and S0 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: s1 if p s1 → s2 ATM 1 Bank operations (non-atomic) ATM 1 Get balance = $1000 Output $100; Calculate new balance = $900 ATM 2 Account $1000 Get balance = $1000 ATM 2 Bank operations (Atomic) ATM 1 Get balance = $1000 Output $100; Calculate new balance = $900 Update new balance $900 $900 Get balance = $900 Output $100; Calculate new balance = $900 Update new balance $800 $900 ATM 2 Account $1000 Update new balance Output $100; Calculate new balance = $900 Update new balance Incorrect Figure 1 Correct 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 28 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 transaction—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 () (1) where s1 and s2 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 types such as arrays and FIFO queues to make the descriptions more readable. With proper abstractions, we can create TRS descriptions in a highly modular fashion. And using a compiler for hardware synthesis from TSRs, such descriptions can be translated into a standard hardware description language like Verilog. By restricting the generated Verilog to be structural, commercial tools can be used to go all the MARCH 2008 | embedded systems design | www.embedded.com http://www.embedded.com

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

Embedded Systems Design - March 2008 Contents #Include Programming Pointers Designing DSP-based Motor Control Using Fuzzy Logic Hardware/Software Verification Enters the Atomic Age Efficient CRC Calculation with Minimal Memory Footprint Programming Your Own Microcontroller Advertising Index Break Points Marketplace

Embedded Systems Design - March 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.