as a PDF
Contents
1. SLA 05 pages 365 383 2005 PCI SIG Conventional PCI 3 0 PCI X 2 0 and PCI E 2 0 Specifications http www pcisig com R Pellizzoni B D Buy M Caccamo and L Sha Coscheduling of real time tasks and PCI bus transac tions Technical report University of Illinois at Urbana Champaign 2008 Available at http netfiles uiuc edu rpelliz2 www R Pellizzoni P Meredith M Caccamo and G Rosu Bus MOP a runtime monitoring framework for PCI peripher als Technical report University of Illinois at Urbana Champaign 2008 Available at http netfiles uiuc edu rpelliz2 www Xilinx Inc Virtex 4 ML455 PCI PCI X Development Kit User Guide http www xilinx com support documentation boards_and_kits ug084 pdf http fsl cs uiuc edu2. COTS components introduce challenges in the devel opment of critical systems as they are unpredictable and often complete hardware specification is not publicly avail able In this paper we have proposed run time monitoring of bus activities as a way to cope with such unpredictabil ity A monitoring device can be plugged on a PCI bus segment and check that all communication between periph erals and the rest of the system behaves according to spec ifications Monitoring logic is automatically generated by the BusMOP framework and synthesized on FPGA result ing in zero CPU runtime overhead Finally we showed the applicability of our monitoring infrastructure and recov ery mechanisms on a real test case We plan to extend this work in two directions From a system point of view we plan to develop a interposing PCI PCI X PCI E monitoring device capable of executing preventive recovery actions as described in Section 4 From a formal specification point of view we plan to extend Bus MOP to support other logic specifications Most of the plu gins already developed for the MOP framework will re quire little work with the exception of context free gram mars CFG which would require implementing effec tively a hardware LR 1 parser This extension is not triv ial the monitor must be able to process each event in few clock cycles but a LR 1 parser can perform an unbounded number of reductions each event Finally none of the for
3. For a vast category of errors that involves incorrect in teraction between the peripheral and its software driver it is often possible to recover from the failure by forcing the pe ripheral into a consistent state The monitoring device im plements a master module and can therefore initiate trans actions on the bus For example consider a common type of error where the driver fails to validate some input from the user and as a result writes an invalid value to a regis ter in the peripheral We can recover by rewriting the reg ister with a valid value However if the error is caused by a fault in the peripheral hardware interacting with regis ters may not be enough to bring the peripheral to a consis tent and safe state 1 We also plan to extend our design to PCI E see Section 8 We propose a mechanism that lets the monitoring device disconnect the faulty peripheral from the bus We developed a simple hardware device the peripheral gate 19 that is able to force the REQ signal from the peripheral to the bus arbiter to be high hence the peripheral never receives the grant and it is prohibited from initiating any further transac tion on the bus The peripheral gate is implemented based on a PCI extender card i e a debug card that is interposed between the peripheral card and the bus and provides easy access to all signals A clarifying picture for monitoring of a single peripheral is provided in Figure 3 a The mon
4. O space followed by one or multiples data phases each of which carries up to 32 or 64 bits of data for PCI PCI X re spectively individual bytes can be masked using byte en ables Since each bus segment is shared arbitration is re quired to determine which master peripheral is allowed to transmit at any one time Arbitration uses two active low point to point wires between the peripheral and the bus seg ment arbiter REQ and GNT A standard request grant handshake is used where the peripheral first lowers REQ to request access to the bus and the arbiter grants permis sion to start a new transaction by lowering GNT 4 Monitoring Device We designed a prototype monitoring device based on a Xilinx ML455 board 21 using a mixed VHDL Verilog reg ister transfer level RTL description The board is outfitted with a Virtex 4 FPGA and is can be plugged into a stan dard 3 3Volts PCI PCI X socket The FPGA implements both a slave and a master peripheral module together with the monitoring modules Events for the system are speci fied in terms of read write data transfers on the bus and in terrupt requests the device continuously sniffs all ongo ing activities on the bus and it is therefore able to moni tor communication for all other peripherals located on the same bus segment Whenever a failure to meet the specifi cation is detected the device can execute a recovery action using strategies based on the detected error
5. check a COTS data acquisition board Our experimental results re veal that the monitoring device is able to detect and recover from errors caused by faults in the driver that we discovered after manually inspecting it We conclude by discussing re lated work in Section 7 and providing final remarks and fu ture work in Section 8 Processors ERE Plugin Figure 2 MOP Architecture 2 The MOP Framework Monitoring Oriented Programming MOP 6 and cita tions there is a formal framework for system development and analysis in which the developer specifies desired prop erties using definable specification formalisms along with code to execute when properties are violated or validated it is important to note that a failure to confirm to the specifi cation can be expressed as either the validation or violation of a property see Section 6 for examples Monitoring code is then automatically generated from the specified proper ties and integrated together with the user provided code into the original system MOP is a highly extensible and config urable runtime verification framework currently there are two MOP instances JavaMOP and BusMOP the instance described in this paper Property specifications consist of event definitions which are instance dependent e g pointcuts in Java MOP and bus transactions or interrupts in BusMOP and logical formulae or patterns which are not The user is al lowed to extend the MOP
6. fear of losing competi tive edge and because the increase in performance is often matched by a similar increase in design complexity out of order execution and branch prediction are examples of this trend in CPU design Modern COTS peripherals run ning in master mode are particularly challenging A mas ter peripheral can directly communicate with all other ele ments in the system including main memory and other pe ripherals thus reducing the load on the CPU On the other side providing fault containment becomes extremely hard a misbehaving low criticality master peripheral could very well disrupt the entire system Based on the above discussion our proposal for the safe integration of COTS peripherals in critical embedded sys tems is to use runtime monitoring the peripheral require ment specifications are checked at runtime against its cur rent observable behavior If any violation is detected then a suitable recovery action can be taken to restore the sys tem to a safe state The validity of the runtime monitoring approach has been proved in the field of software engineer ing by a large number of developed tools and techniques see Section 7 However applying runtime monitoring to our scenario poses some new challenges First of all the be havior of a COTS peripheral is controlled both by the hard ware of the peripheral itself and by its software driver hence we must check the correctness of their interactions Second
7. malisms supported so far include the notion of time as an explicit variable making it difficult to check real time re quirements As a long term research goal to solve this prob lem we plan to develop efficient runtime monitoring algo rithms for a significant subset of timed automata 1 References 1 R Alur and D L Dill A theory of timed automata Theoret ical Computer Science 126 183 235 1994 2 P Avgustinov A Christensen L Hendren S Kuzins J Lho tak O Lhotak O de Moor D Sereni G Sittampalam and J Tibble ABC an extensible AspectJ compiler In Proc of the ACM Conf on Aspect oriented software development ASOD 05 pages 87 98 2005 3 P Avgustinov J Tibble and O de Moor Making trace mon itors feasible In Proc of the ACM Conf on Object Oriented 4 More precisely MOP supports DCFLs 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 Programming Systems Languages and Applications OOP SLA 07 pages 589 608 2007 H Barringer A Goldberg K Havelund and K Sen Rule based runtime verification In Int Conf on Verification Model Checking and Abstract Interpretation VMCAI 04 pages 277 306 2004 BusMOP webpage BusMOP F Chen and G Ro u MOP An Efficient and Generic Run time Verification Framework In Proc of the ACM Conf on Object Oriented Programming Systems Languages and
8. not have specified value ranges The reason for this is that when a value range is specified the code generator must gener ate the proper byte enables based on address alignment and alignment does not make sense for ranges Address ranges are useful for some properties e g a property that moni tors accesses to a certain buffer in memory 5 2 The bus_interface Module The code for the declarations and handler sec tions is copied verbatim into the VHDL module defin ing the bus interface Because of this copying the code must be written in VHDL The events are expanded to com binatoric statements implementing the specified logic The output of the combinatoric statements is assigned to an events wire vector which is connected to the monitor mod ule through an event sequentializer submodule Each index in the bus corresponds to the truth value of a spe cific event numbered with the 0 th index as the first event and the n th index as the n th event from top to bot tom in the specification This ordering is important be cause it directs the event linearization performed by the event_sequentializer submodule The event_sequentializer is necessary because the log ical formalisms expect linear disjoint events The event_sequentializer takes coincident events and sends them to the monitor in subsequent clock cycles in as cending index order using the seq_events wire vector Therefore if events 0 and events 3 occur in t
9. of the formula and it is the only portion of our system de pendent on the logical formalism used Extended Regular Expressions Extended regular ex pressions EREs are the normal regular expressions 16 extended with negation The same plugin used for Java MOP s 6 EREs is used to transform the provided ERE to a minimized deterministic finite automata DFA defined in generic code We convert the generic code to Verilog The current state of the DFA is kept in a register On each clock cycle the current state of the DFA and the event are con sulted to see if the property is violated or validated and what state to transition to Violations of EREs are tricky because if used normally a DFA once it reaches a viola tion state will report a violation every event because there is no valid transition out of the violation state We chose to reset the DFA to the initial state whenever a violation is en countered to avoid this problem ERE pattern is as follows Pattern epsilon Event Name Pattern Pattern Pattern Pattern Pattern Pattern a epsilon is the empty string is negation is zero or more repetitions is logical or and Pattern Pattern represents concatenation Past time Linear Temporal Logic Past time Tempo ral Linear Logic PTLTL 8 extends normal propositional logic with temporal operators We modified the PTLT
10. real time computation To combat these problems we propose a distributed monitoring technique based on the development of a mon itoring device The idea is to introduce an additional hard ware component into the system that can check all periph eral communication and perform recovery actions when necessary Assuming sniffing data transfers does not add delay to the system our solution prevents the first type of overhead The second type of overhead is removed by run ning all monitors directly on the device adding no runtime overhead to the CPU Additionally the system can run com pletely undisturbed as long as no recovery action is needed The speed of modern COTS communication architec tures rules out the possibility of a software implementation for the device instead all logic is implemented on a recon figurable FPGA Finally to show that a monitored system is safe we need to prove that the monitoring logic moni tors indeed the right properties In our system this is en sured by automatically synthesizing the monitoring logic from formal requirements specification so that it is cor rect by construction In particular we leverage on the Mon itor Oriented Programming MOP 6 framework see Sec tion 2 which is highly extensible and supports multiple for malisms by creating a new MOP instance BusMOP Illustrative Example An example of BusMOP can be seen in Figure 1 This example is a property used in the
11. therefore VHDL seems well suited to the task As can be seen in the Figure 3 b the monitor mod ule reports the validation violation or neutral state of the monitored property via the properties wire vector to the bus_interface module Several actions are available in vali dation and violation handlers Aside from manipulating any local state of the monitor such as the write to cntrlCurrent in Figure 1 the bus_interface module makes available sev eral registers which can be used used to execute the recov ery actions detailed in Section 4 The registers are summa rized in the table below Write Interface io_reg write request in I O space mem_reg write request in memory space address_reg write address value_reg write value enable_reg byte enables serial_reg ASCII value to serial output stop_reg Peripheral gate control As can be seen in Figure 1 we perform a memory write to the cntr_cntrl2 register of its previous value The ad dress_reg is used to denote the address of cntr_cntrl2 base1 X 202 while the value_reg is set to the old value of cntr_cntrl2 the mem_reg is asserted to tell the PCI bus that the write performed is a memory write and the byte en ables are set to 0011 to denote that the lower two bytes must be written 5 3 The monitor Module The monitor module is responsible for monitoring the property given serialized events It encompasses the logic
12. Applications OOPSLA 07 pages 569 588 2007 D Drusinksky Temporal rover 1997 2007 E A Emerson Handbook of Theoretical Computer Science MIT Press 1990 Chapter 16 Temporal and modal logic Eagle Technology PCI 703 Series User s Manual http www eagledaq com display_product_36 htm D Abramson et al Intel virtualization technology for di rected i o Intel Technology Journal 10 03 Aug 2006 K Havelund and G Rosu Monitoring Java programs with Java pathexplorer In Proc First Workshop on Runtime Veri fication 2001 K Hoyme and K Driscoll Safebus tm JEEE Aerospace Electronics and Systems Magazine pages 34 39 Mar 1993 M Kim M Viswanathan S Kannan I Lee and O Sokol sky Java mac A run time assurance approach for Java pro grams Formal Methods in System Design 24 2 129 155 2004 D Knuth Backus normal form vs backus naur form Com munications of the ACM 7 12 735 736 1964 H Lu and A Forin The design and implementation of p2v an architecture for zero overhead online verification of soft ware programs Technical Report MSR TR 2007 99 Mi crosoft Research 2007 M Sipser Introduction to the Theory of Computation PWS Publishing 1996 Chapter 1 Regular Languages M Martin B Livshits and M Lam Finding application errors and security flaws using PQL a program query lan guage In Proc of the ACM Conf on Object Oriented Pro gramming Systems Languages and Applications OOP
13. Hardware Runtime Monitoring for Dependable COTS based Real Time Embedded Systems Rodolfo Pellizzoni Patrick Meredith Marco Caccamo Grigore Ro u Department of Computer Science University of Illinois at Urbana Champaign rpelliz2 pmeredit mcaccamo grosu cs uiuc edu Abstract COTS peripherals are heavily used in the embed ded market but their unpredictability is a threat for high criticality real time systems it is hard or impossi ble to formally verify COTS components Instead we pro pose to monitor the runtime behavior of COTS peripherals against their assumed specifications If violations are de tected then an appropriate recovery measure can be taken Our monitoring solution is decentralized a monitoring de vice is plugged in on a peripheral bus and monitors the peripheral behavior by examining read and write trans actions on the bus Provably correct w rt given speci fications hardware monitors are synthesized from high level specifications and executed on FPGAs result ing in zero runtime overhead on the system CPU The pro posed technique called BusMOP has been implemented as an instance of a generic runtime verification frame work called MOP which until now has only been used for software monitoring We experimented with our tech nique using a COTS data acquisition board 1 Introduction The real time embedded system industry is progres sively moving towards the use of Commercial Off The Shelf COT
14. L plu gin used in JavaMOP to make it more suitable for imple mentation as a logic circuit The original generic code out put by the plugin used a number of sequential assignments to an array of truth values We take this sequential code and using back substitution change the sequential code into a series of parallel assignments The resulting assignments are entirely parallel allowing the operation of the monitor to be contained within a single clock cycle A more in depth explanation of this transformation is omitted but will ap pear in an upcoming technical report on PTLTL The syn tax for PTLTL formulas is as follows Formula true false Event Name not Formula Formula and Formula Formula or Formula Formula implies Formula Cx Formula Formula x Formula Formula S Formula not and or and implies are the ordinary logic operators x x and S are temporal opera tors denoting always in the past eventually in the past pre viously and since respectively As an example of the transformation to efficiently moni torable code consider the PTLTL formula grant implies request This formula states that if a grant of some resource occurs then at some point in the past there must have been a request gt This results in sequential code b 0 request or
15. S components in an attempt to reduce costs and time to market even for highly critical sys tems like those deployed by the avionic industry While specialized hardware and software solutions are some times available for such markets their average performance and ease of integration is lagging behind the develop ment of COTS components For example a commercial plane like the Boeing 777 uses the SAFEbus back plane 12 which while specially designed to meet the This material is based upon work supported by Lockheed Martin Aeronautics under contract PO 7142310 and NSF under Awards No CNS0237884 CNS0720512 CNS0613665 Any opinions findings and conclusions or recommendations expressed in this publication are those of the authors and do not necessarily reflect the views of the NSF hard real time constraints of an avionic system is only ca pable of transferring data up to 60 Mbps On the other side a modern COTS peripheral bus such as PCI Ex press 2 0 18 can reach transfer speeds of 16 Gbyte s over three orders of magnitude greater than SAFEbus Unfortunately when trying to use COTS for building high integrity real time embedded systems current engi neering practices face significant challenges While one can capture relevant assumptions about COTS as formal spec ifications they are hard or impossible to formally verify this is both because manufacturers are unwilling to disclose details of their implementation for
16. b 0 output not grant or b 0 b is the array of truth values used by the monitoring algorithm each truth value becomes a single bit flip flop in the FGPA implementation The state ment output tells us what the output state of the monitor is i e at a given time event arrival the original formula is true if b 0 is true Because this is sequential code it is signifi cant that output is the last statement it need not necessarily be last grant implies request is changed to not grant or request by boolean simplification If we evaluate the se quential code for a simple trace request grant we see that when request arrives b 0 is assigned the value true regard less of the previous value of b 0 and that true is output If the output statement were first the output would be false on the first request event When the grant arrives the moni tor again outputs true because b 0 is true In order to transform this into a series of parallel as signments we need substitute the rhs R of an assignment statement bfi R into all assignments b j R af ter b i R such that b i R The reason for this is that with parallel assignments all rhs are evaluated before any assignments occur The final parallel assignment code de noted by rather than is b 0 request or b 0 output not grant or request or b 0 As we can see request or b 0 has been substituted for the original reference to b 0 the re maining b 0
17. case study of Section 6 and related to the behavior of Counter 2 a counter on the PCI703A board we used in our experiments This property called SafeCounterModify requires that any modification to cntr_cntrl2 the control register for Counter 2 happens only while the counter is not in use This modifi cation is captured by the cntriMod event because cntr_cntrl2 is at address X 220 The counter can be enabled disabled by modifying bit 0 of cntr_cntrl2 captured by the countEn able countDisable events is the VHDL don t care The declarations section declares two monitor local reg isters cntriCurrent and cntrlOld and initializes them to 0 These registers will hold the current and previous values of the cntr_cntrl2 register This allows us to repair the regis ter when if the property is violated by writing the old value to the register on the peripheral itself the value_reg assign ment and forcing the current value the monitor stores to be the previous value as can be seen in the violation han dler section of the specification The ere pattern itself in the ere section matches any trace that consists of a cntr_cntrl2 modification a disable of the counter or an enable followed by a disable The pat tern is followed by allowing it to match repeatedly The only way to violate this pattern then is to see a modifica tion after an enable that is not followed by a disable first The implementation of th
18. contains the value from the previous event A design decision relating to both logics we have imple mented and all future logics is that properties cannot be vi olated or validated before an event arrives Without this as sumption the example ERE property would be valid at start up This creates a problem to correctly trigger recovery ac tions in the bus_interface module we require that the prop erties wire be set to 1 2 for a validation violation respec tively for only one clock cycle The solution we adopted is simply to set properties to zero when no event is detected An additional problem is that without the assumption a sin gle event in ERE could cause a violation followed immedi ately by a validation since we reset the monitor on viola tion in the same clock cycle This could in turn trigger both a validation and violation handler at the same time which is something we can not support JavaMOP has the same func tionality but in JavaMOP it is due to the fact that a moni tor does not exist before the first event whereas in BusMOP the monitor exists as soon as the FPGA is configured 3 This property is over simplified multiple grant s are allowed for one request 6 Case Study The PCI703A ADC DAC Board In this section we show how our runtime monitoring technique can be applied to a concrete case by providing specification and runtime experiments for a specific COTS peripheral the PCI703A board 9 PCI703A
19. ct PCI is the cur rent standard family of communication architectures for motherboard peripheral interconnection in the personal computer market it is also widely popular in the embed ded domain 18 The standard can be divided in two parts a logical specification which details how the CPU config ures and accesses peripherals through the system controller and a physical specification which details how peripher als are connected to and communicate with the mother board While the logical specification has remained largely unaltered since the introduction of the original PCI 1 0 stan dard in 1992 several different physical specifications have emerged since then One of the main features of the logical layer is plug and play automatic configuration functionality On start up the OS executes a PCI base driver which reads infor mation from special configuration registers implemented by each PCI compliant peripheral and uses them to configure the system Of peculiar importance is a set of up to 6 Base Access Registers BARs Each BAR represents a request by the peripheral for a block of addresses in either the I O or memory space the PCI base driver is responsible for ac cepting such requests allocating address blocks and com municating back the chosen addresses to the peripheral by writing in the BARs To communicate with the peripheral the CPU can then issue write and read commands called transactions to either I O or mem
20. ctions that target that specific peripheral or are initiated by it If a property is validated violated it is then possible to take preventive measures i e either dis card or modify the transaction before propagating it While this solution will provide a higher degree of reliability there is a price to be paid in terms of increased communication delay due to buffering in the monitoring device A simplified block diagram for the monitoring device is shown in Figure 3 b We distinguish three types of blocks 1 blocks provided by Xilinx as proprietary intel lectual properties IPs 2 manually coded RTL modules provided by BusMOP which are independent of the periph eral specification 3 automatically generated RTL modules which are dependent on the specification see Section 5 PCI transaction signals are routed to two different modules 2 While technically it is always possible for a faulty peripheral to disrupt the bus by altering the state of the signals in practice the described ap proach is effective since access to the bus is mediated by three state buffers enabled by GNT decoded data Peripheral manually written Poy automatically generated L provided IP Monitoring Device a Gated Monitoring Device RS232_interface master b Block Diagram Figure 3 Monitoring Device the PCl_core and the decode module The PCl_core module is a hard IP that implements all logic required
21. d memory write address in base1 X 228 divrOld lt divrCurrent divrCurrent lt value 15 downto 0 event countEnable memory write address base1 X 220 dbyte value in 1 ptltl divrMod and mot countDisable S countEnable validation handler mem_reg lt 1 address_reg lt base1 X 228 roll back to the previous cntr_divr2 value value_reg 15 downto 0 lt divrOld divrCurrent lt divr0ld enable_reg lt 0011 Figure 8 SafeDivrModify Specification Rove 7 is a commercial runtime verification tool which uses future time metric temporal logic It provides inline specification of monitors where the monitors are written straight in the source file Inline specification does not make sense for BusMOP as there is no program being monitored per se Program Query Language PQL 17 is an approach somewhat similar to MOP although it also only allows one specification language PQL can support the full general ity of context free languages Tracematches 3 is very sim ilar to JavaMOP The biggest difference is that its choice of regular expressions for logical formalism is hardwired It is an extension of the AB 2 AspectJ compiler All of the above approaches are designed to monitor specific pro grams and are implemented in software This has the effect of both adding runtime overhead and performing a func tion different from that of BusMOP which monitors COTS p
22. e events declarations and the actions available to handlers is explained in Section 5 2 The formula pattern implementation and the use of handlers is explained in Section 5 3 The actual generated code is avail able in our Technical Report 20 or by running the online trial on our website 5 Key contributions We provide three main contribu tions First in Section 4 we describe the design of a mon itoring device for the PCI PCI X bus a brief overview of PCI is presented in Section 3 The monitoring device can be plugged in on a PCI bus segment and monitor all periph erals attached to the segment Whenever peripheral activ ity fails to conform to the specification the device can per form a corrective action either bring the peripheral back to a safe state if the error is recoverable or otherwise discon nect it from the system While certain implementation deci sions are necessarily specific to our choice of PCI we be lieve that the general design principles and lessons learned can be applied to most other communication architectures Second in Section 5 we provide a new instantiation of the MOP framework called BusMOP that is able to generate hardware modules the generated monitoring logic is then integrated with the rest of the monitoring device design and synthesized on the FPGA Third in Section 6 we show the feasibility of the overall approach by applying our technique together with the developed monitoring device to
23. er Timers block implements four counters Counter 0 and 1 are user programmable and can be used either for debugging purposes or to trigger a DA conversion Counter 3 is also user programmable and pro duces an external output Finally Counter 2 is not meant to be user programmable it is to be used exclusively to gener ate the clock for AD conversions The C user library pro vided with the driver exports an ADConfig function used to configure ADC Control and the associated Counter 2 The library also provides a CTConfig function to be used to configure the user counters unfortunately under Linux the function can also be used to change the configuration of Counter 2 This is a problem as any user in the system could erroneously or maliciously change Counter 2 while an ADC is in progress Three 16 bits control registers are relevant to our dis cussion cntr_cntrl2 at hexadecimal location 220 rela tive to BAR1 cntr_divr2 228 and adc_cntrl 300 Bit O of cntr_cntrl2 determines whether Counter 2 is en abled and bits 2 1 determine its clock source either 20Mhz or 100Khz when the counter is enabled it first loads the content of cntr_divr2 and then starts count ing down at the selected frequency When it reaches zero the value of cntr_divr2 is reloaded a clock sig nal is sent to ADC Control and finally if bit 4 of cntr_cntrl2 is set an interrupt is generated Register adc_cntrl con trols the behavior of ADC Control in particula
24. eripherals The PSL to Verilog compiler P2 15 is the sole at tempt to perform formal runtime verification in hardware of which we are aware P2V is similar to BusMOP in that monitors are implemented in hardware rather than soft ware and that both approaches thus have no runtime over head on the CPU P2V however is more like the above ap proaches in that it is designed for monitoring actual pro grams rather than peripheral devices Also it requires a dy namically extensible soft core processor implemented on an FPGA while our approach can potentially be applied to any COTS communication architecture Further P2V uses hard wired logic while BusMOP allows different formalisms Finally in recent years there have been several propos als in the industry to extend virtual memory support to pe ripherals for example see 10 While the main objective of these mechanisms is to extend virtualization to hardware devices they can nevertheless be used to improved system reliability preventing peripherals from writing to wrong lo cations in main memory In comparison BusMOP is able to check a much greater range of requirements but in its cur rent implementation it lacks the ability to take preventive measures As such it can be beneficial to use both tech niques together to simplify recovery 8 Conclusions and Future Work COTS peripherals are increasingly being adopted in the embedded market for performance reasons How ever
25. framework with his her own logics via logic plugins which encapsulate the monitor syn thesis algorithms This extensibility of MOP is supported by a layered architecture which separates monitor genera tion and monitor integration By standardizing the protocols between layers modules can be added and reused eas ily and independently By providing language specific shells logic plugins can be reused between several dif ferent MOP instances A graphical representation of the architecture can be seen in Figure 2 The formula or pattern designates which traces ob served series of events are valid or invalid Because ex tended regular expression ERE and past time linear tem poral logics PTLTL are the two plugins used in this paper we will describe which traces are valid or invalid for ERE patterns and PTLTL formulae For EREs valid traces are those which are strings in the language represented by the ERE with events treated as the letters in the alphabet of the language Neutral traces which trigger no handlers are pre fixes of strings in the language while violations are invalid strings For PTLTL formulae valid traces are any traces for which the formula evaluates to true invalid traces are those for which the formula evaluates to false there are no neu tral traces For more information on regular languages and temporal logic see 16 and 8 respectively 3 PCI Bus Overview The Peripheral Component Interconne
26. he same cy cle the monitor will see 0 followed by 3 To see why si multaneous events are possible consider again Figure 1 from Section 1 The cntriMod event is asserted when ever the cntr_cntrl2 register base1 X 220 is written Because both the countEnable and countDisable events re quire writes to the same address as the cntrlMod event any time countEnable or countDisable are triggered a cntrliMod is also triggered As the property tries to enforce the pol icy that all modifications happen when the counter is not enabled we must serialize events such that cntrlMod hap pens after a countDisable and before a countEnable The ordering of events in Figure 1 is consistent with this be cause countDisable is listed before cntriMod which is listed before countDisable The violation handler is placed in the module such that it is only executed if the monitor module denotes that the prop erty has been violated The situation is similar for a valida tion handler save that it is executed only when the formula or pattern is validated Currently recovery actions in the handlers are specified as a list of concurrent VHDL state ments While it could be possible to define a new formalism for recovery specification we believe it would not be very beneficial for two main reasons the formalism would have to be specific to BusMOP specifying correct recovery ac tions inevitably requires a deep understanding of the mon itored hardware
27. irement 3 and can be seen in Figure 7 This could have been written in a similar manner to SafeConver sionSpeed i e using event side effects to store current register values and checking them in the handler We de cided to use a fully formal specification that defines events for setting the registers to good or bad values The for mula itself specifies that if the ADC is enabled and clkSrc2 is good meaning that Counter 2 is being used to time the ADC then Counter 2 must be enabled The part of the for mula before the implies keyword states that the ADC is enabled and the ADC clock source is Counter 2 the sec ond half of the formula is the requirement that Counter 2 not be disabled The formula is true when correct behav ior is exhibited so we use a violation handler for the re covery action which again is simply to set cntr_cntrl2 to the last valid value SafeDivrModify The SafeDivrModify specification is the formalization of part of Requirement 3 and can be seen in Figure 8 In conjunction with NoDisableWhileConvert ing and SafeCounterModify from Section 1 all of require ment 3 is covered This specification ensures that cntr_divr2 is not modified while Counter 2 is enabled This property is the same as SafeCounterModify from Figure 1 save that we are ensuring that cntr_divr2 is not modified rather than cntr_cntrl2 We also used PTLTL rather than ERE to show how two very similar properties look in both logics These c
28. is a high per formance Analog to Digital Digital to Analog Conversion ADC DAC peripheral for the PCI bus In particular it can perform high speed 14 bits precision ADC at a rate of up to 450 000 conversions s and transfer data to main mem ory in bus master mode At the same time the peripheral is simple enough that we were able to carefully check all pro vided hardware manuals and to manually inspect its Linux driver specifying formal properties for a peripheral clearly requires a deep understanding of its inner working In our proposed model the peripheral s manufacturer is responsi ble for writing the runtime specification In this sense the formal specification can be thought of as a correctness cer tification provided by the manufacturer as long as the user employs a monitoring device and recovery actions can be proved to restore the system to a safe state To better mimic what we think would be a typical pro cess for a COTS manufacturer we produced a requirement specification for the PCI703A in two steps First we pre pared a detailed description of the communication behav ior of the peripheral in plain English Then we converted this informal description into a formal set of events and for mulae for BusMOP Inspection of the driver revealed two software faults both of which can cause errors that are de tected and recovered by the monitoring device While in this case we could have prevented errors by simply removing
29. itoring device can output a stop signal which closes the gate when active high Finally sometimes the monitoring device cannot perform a suitable recovery action by itself but there is a higher level actor such as the OS or the sys tem user that can provide better recovery examples include complex software operations such as restarting the driver or the whole PCI stack and physically interacting with the pe ripheral In this case the best strategy is to communicate the failure to the chosen actor The study of OS level reliabil ity techniques is outside the scope of this paper instead for our prototype design we implemented a RS 232 controller that can be used to send information to the user over a se rial connection The reader should notice that the nature of our imple mentation is such that if a trace is seen which does not con form to a specification as a consequence of a bus trans action that specific bus transaction can not be prevented from propagating to the rest of the system For example if a faulty peripheral performs a write transaction to an area in main memory which is not supposed to modify we can de tect the error disconnect the peripheral and report the fail ure to the OS user However the information in the over written area will be lost As part of our future work we are working to implement an interposed monitoring device by sitting between the bus and a peripheral it will be able to buffer all transa
30. master peripherals can directly interact with the rest of the system without requiring any action by the CPU Based on these two considerations our monitoring solution must be able to detect and check all communication between the pe ripheral and the rest of the system Finally runtime moni declarations signal cntrlCurrent STD_LOGIC_VECTOR 15 downto 0 X 0000 signal cntrl0ld STD_LOGIC_VECTOR 15 downto 0 X 0000 F event countDisable memory write address base1 X 220 dbyte value in o event cntrlMod memory write address in base1 X 220 cntrl0ld lt cntrlCurrent cntrlCurrent lt value 15 downto 0 event countEnable memory write address base1 X 220 dbyte value in 1 ere countEnable countDisable cntrlMod countDisable violation handler mem_reg lt 1 address_reg lt basei X 220 roll back to the previous cntr_cntrl2 value value_reg 15 downto 0 lt cntrl0ld cntrlCurrent lt cntrl0ld enable_reg lt 0011 Figure 1 Example Property SafeCounterModify toring typically comes with an unforgivable price runtime overhead We can split such overhead in two components 1 overhead due to the observation and generation of rele vant events 2 overhead due to running a monitor at each event to check if any property of the specification is vio lated Both types of overhead tend to be unpredictable and thus unsuitable for
31. ory space each periph eral is required to implement bus slave logic which decodes and responds to transactions targeting all address spaces al located to the peripheral Typically address spaces are used to implement either registers which control and determine the logical status of the peripheral or data buffers Periph erals can also implement bus master logic they can au tonomously initiate read and write transactions to either main memory or the address space of another peripheral Master mode is typically used by high performance periph erals to perform a DMA transfer i e transfer data from the peripheral to a buffer in main memory The peripheral s driver can then read the data directly from memory which is much faster than issuing a read transaction on the bus Fi nally each peripheral is provided with an interrupt line that can be used to send interrupts to the CPU There are two main flavors of physical architecture PCI PCI X is parallel while PCI E is serial but runs at much higher frequency 2 5Ghz against up to 133Mhz for PCI X We have focused on PCI PCI X which imple ments a shared bus architecture The logical PCI tree is physically divided into bus segments and most bus wires are shared among all peripherals connected to a single seg ment We refer to 18 for detailed bus specifications Each transaction seen on the bus consists of an address phase which provides the initial address in either memory or I
32. ould be collapsed into one specification but it would make recovery more complicated because we only want to roll back the register that was actually modified cntr_cntrl2 or declarations signal cntrlCurrent STD_LOGIC_VECTOR 15 downto 0 X 0000 signal cntrl0ld STD_LOGIC_VECTOR 15 downto 0 X 0000 event countEnable memory write address base1 X 220 dbyte value in n cntrl0ld lt cntrlCurrent cntrlCurrent lt value 15 downto 0 event countDisable memory write address base1 X 220 dbyte value in o cntrl0ld lt cntrlCurrent cntrlCurrent lt value 15 downto 0 event clkSrc2Good memory write address base1 X 300 dbyte value in 01 event clkSrc2Bad memory write address base1 X 300 dbyte value not in o1 event adcEnable memory write address base1 X 300 dbyte value in 1 event adcDisable memory write address base1 X 300 dbyte value in o ptltl not adcDisable S adcEnable and not clkSrc2Bad S clkSrc2Good implies not countDisable S countEnable violation handler mem_reg lt 1 address_reg lt base1 X 220 roll back to the previous cntr_cntrl2 value value_reg 15 downto 0 lt cntrl0ld cntrlCurrent lt cntrl0l1d enable_reg lt 0011 Figure 7 NoDisableWhileConverting Specification cntr_divr2 The formula it
33. r bit 0 enables disables the ADC process and bits 2 1 deter mine the clock source with a value of 00 indicating that Counter 2 is used We express three requirements Requirement 1 Bit 4 of cntrcntri2 should never be set While the functionality is relevant for Counters 0 1 in the case of Counter 2 setting bit 4 would cause the generation of spurious interrupts that increase load on the driver Requirement 2 Jf the ADC is using Counter 2 and the clock source for Counter 2 is set to 20 Mhz then the value of cntr_divr2 must be at least 45 to avoid violating the max imum conversion speed of the peripheral declarations signal cntrlCurrent STD_LOGIC_VECTOR 15 downto 0 X 0000 signal cntrl0ld STD_LOGIC_VECTOR 15 downto 0 X 0000 F event cntrlMod memory write address in base1 X 220 cntrl0ld lt cntrlCurrent cntrlCurrent lt value 15 downto 0 event setBit4 memory write address base1 X 220 dbyte value in i ere setBit4 validation handler mem_reg lt 71 address_reg lt basel X 220 roll back to the previous cntr_cntrl2 value value_reg 15 downto 0 lt cntrl0ld cntrlCurrent lt cntrl0ld enable_reg lt 0011 Figure 5 InterruptFix Specification Requirement 3 Jf the ADC is active and using Counter 2 then Counter 2 must also be active furthermore while Counter 2 is active no change to the counter configuration is allowed Requi
34. rements 1 3 are able to catch the driver bug in the sense that an invalid counter configuration can not be set before starting the ADC and furthermore while the ADC is active no counter modification is allowed We wrote four five including the example from Section 1 formal proper ties to capture the requirements InterruptFix The InterruptFix specification is the for malization of Requirement 1 and can be seen in Figure 5 Because we do not want the 4th bit set we simply monitor the pattern setBit4 an event which corresponds to setting the 4th bit We perform recovery when the pattern is val idated by overwriting cntr_cntrl2 with the last valid value similarly to SafeCounterModify in Figure 1 SafeConversionSpeed The SafeConversionSpeed spec ification is the formalization of Requirement 2 and can be seen in Figure 6 For this property we chose to show how event side effects can be used in handlers as part of check ing that a property has been validated violated When the clkSrcSet or srcSet events are triggered meaning that the entr_cntrl2 or adc_cntrl registers have been modified respec tively we store the value written to the register in monitor local registers e g src lt value 15 downto 0 The pat tern specifies that the cntr_divr2 be set to a bad value less than 45 followed by any number of updates to cntr_cntrl2 or adc cntrl followed by the enabling of the counter If cntr_divr2 is set to a value larger than 44
35. self states that if cntr_divr2 has been modified and the counter has not been disabled since the last time it was enabled than we must recover Unlike SafeCounterModify we use a validation rather than a viola tion handler because the formula was easier to express with recovery being on validation As a final consideration note that the handlers of Safe CounterModify InterruptFix and NoDisable WhileConvert ing can be invoked simulteously if an incorrect value is writ ten to cntr_cntrl2 which results in the execution of multiple bus writes However this causes no problem since all han dlers overwrite cntr_cntrl2 with the same valid value 7 Related Work There are two main run time verification approaches 1 offline where a log or trace is kept which can then be used for purposes of debugging and 2 online where a property is checked while the program is running As BusMOP is an online technique we will only describe online approaches to runtime verification MaC 13 PathExplorer PaX 11 and Eagle 4 use specific verification languages which cannot be changed while BusMOP as an extension of MO 6 will eventu ally support all the logics supported in JavaMOP Temporal declarations signal divrCurrent STD_LOGIC_VECTOR 15 downto 0 X 0000 signal divrOld STD_LOGIC_VECTOR 15 downto 0 X 0000 event countDisable memory write address base1 X 220 dbyte value in o event divrMo
36. submodule see Sec tion 5 2 and then passed to monitorl using the seq_events wires monitor checks whenever the formula for the I th property is validated violated and passes the information back to bus_interfacel which can then execute three types of recovery 1 disconnect a monitored peripheral from the bus using the stop signal 2 send information to the user us ing the serial_output module which implements a RS 232 transmitter 3 start a write transaction on the bus using the master module Finally since it is possible for multiple sys teml modules to initiate recovery at the same time we pro vide queuing functionalities for serial_output and master in modules master_queue and serial_queue respectively It is important to notice that in the current implemen tation the time elapsed from any event that triggers a val idation violation to executing the corresponding handler is at most 4 clock cycles This time is short enough to exe cute a recovery action before a faulty peripheral is allowed to start a new transaction as PCI arbitration overhead pre vents a peripheral from transmitting immediately 5 Property Specifications Properties are specified using a domain specific event syntax and formulae or patterns written in the logic of a particular plugin Additional monitor state can also be de clared using the declarations section The violation handler and validation handler sections allow for arbitrary code to be exec
37. the faults we argue that drivers for more complex periph erals can be thousands of lines long and neither code in spection nor testing is sufficient to remove all bugs We fur ther injected additional faults in the driver to test all written formal properties It would have been nice to also show re covery for hardware faults but we did not find any in the tested peripheral and injecting faults in the hardware is dif ficult A list of both informal and formal properties can be found at 20 In what follows we first provide an overview of PCI703A and then we detail properties for an example subsystem a counter used in the ADC process The exam ple is particularly instructive as we show how a small but representative set of properties is able to catch one of the aforementioned driver bug A block diagram for the PCI703A is shown in Figure 4 The bus slave logic implements two memory address blocks in BARO and BARI used for conversion data and control registers respectively the corresponding base ad dresses are written in base0 and base1 in the monitoring de vice The ADC Control and DAC Control blocks control the ADC DAC operations and write read data into internal FI FOs The DMA Control block can be programmed to move data between each FIFO and main memory using bus master ADC DMA Control Control Counter Timers DAC Control Slave Bus Master Bus Logic Logic Figure 4 PCI703A Diagram functionality Finally the Count
38. the pattern will be violated and the monitor will be reset This means that the validation handler will be executed only when then value of cntr_divr2 is too low for safe conversion but regardless of whether or not the board is actually using Counter 2 The handler then checks that it is in fact using Counter 2 and declarations signal clkSrc STD_LOGIC_VECTOR 15 downto 0 X 0000 signal src STD_LOGIC_VECTOR 15 downto 0 X 0000 event divrBad memory write address base1 X 228 dbyte value in 0 44 event divrGood memory write address base1 X 228 dbyte value in 45 65535 event clkSrcSet memory write address in base1 X 300 clkSrc lt value 15 downto 0 memory write address in base1 X 220 src lt value 15 downto 0 event countEnable memory write address base1 X 220 dbyte value in a event srcSet ere divrBad clkSrcSet srcSet countEnable validation handler if clkSrc 2 downto 1 01 and src 2 downto 1 00 then mem_reg lt 71 address_reg lt base1 X 228 set cntr_divr2 to 45 value_reg 15 downto 0 lt X 2D enable_reg lt 0011 end if Figure 6 SafeConversionSpeed Specification that Counter 2 is using the 20Mhz source before perform ing the recovery setting cntr_divr2 to a valid value 45 NoDisableWhileConverting The NoDisableWhile Converting specification is the formalization of part of Re qu
39. ticExp ArithmeticExp ArithmeticExp Number ID ArithmeticExp ArithmeticExp ArithmeticExp ArithmeticExp ArithmeticExp amp ArithmeticExp Number VHDL number or bitstring ID Capital or lower case letter LetterOrDigit LetterOrDigit Capital or lower case letter Digit There are three basic types of events in BusMOP I O accesses memory accesses and interrupts It is impor tant to distinguish between I O and memory events be cause they require different enable functionality and differ ent read write signals We show uses of interrupt events in 20 I O and memory events must specify at least an ad dress which may be an arithmetic expression over identi fiers VHDL numbers addition subtraction and concate nation and whether the event is a read or a write An I O or memory event may also specify a value range which is the value of the address read or written by the bus transac tion Ranges can consist of a single arithmetic expression or a pair of comma separated arithmetic expression denot ing the minimum and maximum values that may trigger the event thus ranges are inclusive Value ranges must also specify a size byte dbyte 16 bits or qbyte 32 bits so that the correct comparison code and byte enables can be generated values smaller than a byte require masking the proper bits Address ranges are used in events that do
40. to handle basic PCI functionalities such as plug and play Bus slave and bus master logic is imple mented by the slave and master modules respectively In particular slave implements a set of 16 registers base0 through base15 Since the OS configures the BAR regis ters at system boot a peripheral cannot directly determine the location of address blocks used by another peripheral Hence the OS must also write the locations of the address blocks allocated to monitored peripherals in the base reg isters The decode module is used to simplify event gen eration It translates all transactions on the bus except for those initiated by the monitoring device itself into a se ries of I O or memory reads writes one for each data phase as well as the occurence of an interrupt and forwards the translated information to the monitoring logic The system0 systeml systemN blocks imple ment the monitoring logic for each of N user specified properties Each systeml block consists of two automati cally generated modules bus_interfacel contains all logic that depends on the specific choice of communication in terface PCI bus while monitorl contains all logic that de pends on the formal language used to specify the prop erty This separation provides good modularity and facili tates code reuse bus_interfacel first receives as input the de coded bus signals and generates events which are sequen tialized by the events_sequentializer
41. uted on the occurrence of a violation or validation re spectively An example of how they are used can be seen in Figure 1 in Section 1 Currently we have support for the extended regular expression ERE and past time temporal logic PTLTL MOP Plugins and adding most of the others will require a minimal amount of work as only the moni tor component changes from one logical specification for malism to another This means that properties may be spec ified formally using an ERE pattern or a PTLTL formula A property is implemented in two main modules a bus_interface which generates logical events from bus traf fic and handles monitor recovery and a monitor implement ing a property specification in hardware A more detailed description will be given below 5 1 Events A formal description of the event syntax using Backus Naur Form BNF 14 extended with p and p denoting zero or one repetitions of p and zero or more repetitions of p respectively can be seen below Event event ID Expression Expression MemoryOrI O ReadOrWrite address ArithmeticExp value not in Range Action MemoryOrl O ReadOrWrite address in Range Action interrupt Action MemoryOrV O memory io ReadOrWrite read write Action Arbitrary VHDL code Range Arithme
Download Pdf Manuals
Related Search