Practical And Veri Able C Dynamic Cast For Hard Real -Books Download

Practical and Veri able C Dynamic Cast for Hard Real
03 Apr 2020 | 13 views | 0 downloads | 30 Pages | 394.83 KB

Share Pdf : Practical And Veri Able C Dynamic Cast For Hard Real

Download and Preview : Practical And Veri Able C Dynamic Cast For Hard Real


Report CopyRight/DMCA Form For : Practical And Veri Able C Dynamic Cast For Hard Real



Transcription

Additional Key Words and Phrases constant time dynamic cast autonomous embedded systems. model based software development static analysis,1 INTRODUCTION. ISO Standard C ISO IEC 14882 International Standard 1998 has become. a common choice for hard real time embedded systems such as the Jet Propul. sion Laboratory s Mission Data System Ingham et al 2004 This is so because. ISO C offers efficient abstraction model good hardware use and predictability. C s model of computation has helped engineers deliver more correct maintain. able and comprehensible software compared to code relying on lower level pro. gramming concepts Stroustrup 2004 However several C features are usually. considered unsuitable for programming real time systems because they do not guar. antee predicable constant time performance Goldthwaite 2006 ISO C does. not provide the necessary timing guarantees for free store heap allocation ex. ception handling and dynamic casting In particular the most common compiler. implementations of the dynamic cast operator traverse the representation of the. inheritance tree at run time searching for a match Such implementations of. dynamic cast are not predictable and are unsuitable for real time programming. Gibbs and Stroustrup G S Gibbs and Stroustrup 2006 describe a technique. for implementing dynamic cast that delivers significantly improved and constant. time performance The key idea is to replace the runtime search through the class. hierarchy with a simple constant time calculation much as the common imple. mentations of the C virtual function calls search the class hierarchy at compile. time to reduce the runtime action to a simple array subscripting operation In the. Journal of Computing Science and Engineering Vol 2 No 4 December 2008. G S scheme a heuristic algorithm assigns an integer type ID at link time to each. class The type ID assignment rules guarantee that at run time a simple modulo. operation can reveal the type information and check the validity of the cast The. requirements for the heuristics assigning the type IDs are that. 1 They must keep the size of the type ID to a small number of bits A 64 bit. type ID should be sufficient for very large class hierarchies. 2 Avoid conflicts and type ID assignments that create ambiguous or erroneous. type resolution at run time,3 Handle virtual inheritance. There are four heuristic schemes and a few possible optimizations suggested in. Gibbs and Stroustrup 2006 However none of those heuristics guarantee the best. solution for every possible class hierarchy The quality of the type ID assignment. heuristics has a critical importance for the performance of the G S scheme With. better heuristics a smaller type ID size would be sufficient to facilitate complex. and large class hierarchies that would certainly need a significantly bigger type. ID size with a poor assignment scheme The main contribution of this work is to. present how the algorithm optimization problem encountered has been successfully. automated and moreover that its automation has led us to quick but significant. improvements of the initial scheme To guarantee a practical and verifiable imple. mentation of the fast dynamic casting scheme we introduce and apply our innova. tive expression template Veldhuizen 1995 based approach for extracting semantic. information from the C source code, Journal of Computing Science and Engineering Vol 2 No 4 December 2008. As pointed out by Lowry Lowry 2002 the increasing complexity of future space. missions such as the Mars Science Laboratory Volpe 2005 and Project Constel. lation Stoica et al 2005 raises concerns whether it is possible to establish their. reliability in a cost effective manner Lowry s analysis indicates that at the present. moment the verification and certification cost of mission critical software exceeds. its development cost Perrow Perrow 1999 studies the risk factors in the modern. high technology systems His work identifies two significant hazard dimensions in. teractions and coupling Complex interactions represent unexpected and unknown. sequences and thus cannot be entirely comprehensible at the time of system de. velopment A tightly coupled system has a number of time dependent processes. that cannot tolerate delays Perrow classifies space missions in the riskiest cate. gory since both hazard factors are present The dominant paradigms for software. development assurance and management at NASA rely on the principle test. what you fly and fly what you test Born out of experience and hindsight this. methodology had been applied in a large number of robotic space missions at the. Jet Propulsion Laboratory For such missions it has proven suitable in achieving. adherence to some of the most stringent standards of man rated certification such. as the DO 178B RTCA 1992 the Federal Aviation Administration FAA soft. ware standard Its Level A requirements demand 100 coverage of all high and. low level assurance policies However the present certification methodologies are. prohibitively expensive for systems of high complexity Schumann and Visser 2006. In this paper we present a co simulation framework based on the SPIN model. checker Holzmann 2003 to simulate evaluate and formally verify the G S fast. Journal of Computing Science and Engineering Vol 2 No 4 December 2008. dynamic casting algorithm and its application in mission critical code such as the. Data Management Services Wagner 2005 of the Mission Data System The aim. of the Mission Data System is to provide a unified state based and goal oriented. architecture for building complete data and control systems for autonomous space. missions The framework s state and model based methodology and its associated. systems engineering processes and development tools have been successfully applied. on a number of test systems including the physical rovers Rocky 7 and Rocky 8 and. a simulated Entry Descent and Landing EDL system for the Mars Science Labo. ratory mission We use the feedback from the model checker to perform systematic. analysis of the G S scheme and look for improvements to the heuristics for type ID. assignment SPIN is an on the fly linear time logic model checking tool that was. designed for the formal verification of dynamic systems with asynchronously exe. cuted processes Model checking tools have been widely applied for the verification. of a large variety of systems including flight software Gluck and Holzmann 2002. network protocols Musuvathi and Engler 2004 and scheduling algorithms Ruys. 2003 We are unaware of work suggesting its use for the analysis and optimiza. tion of compiler heuristics Compiler verification usually focuses on seeking a proof. on the preservation of the program semantics during the various compiler passes. Lerner et al 2003 Our work presents the application of a model checking tool. for the analysis and refinement of the combinatorial optimization problem posed. by the G S type ID assignment scheme Our co simulation framework consists of. the following components, 1 An abstract model of the G S type ID assignment heuristics. Journal of Computing Science and Engineering Vol 2 No 4 December 2008. 2 A procedure for exhaustive search of the state space discovering the best type. ID assignment, The analysis of the heuristics simulation performed in SPIN provides us with ideas.
of possible improvements to the G S type ID assignment We include and evaluate. the proposed improvements in the abstract model in order to seek refinement of the. G S type ID assignment scheme The experiments we have executed show that. the G S priority assignment is not optimal with respect to the best possible type. ID assignment where non virtual multiple inheritance is used While potentially. dangerous if not constructed carefully such hierarchies happen to be of significant. practical importance Stroustrup 2000 Based on our experiments we suggest opti. mizations that lead to significant improvement of the G S heuristics performance. We rely on model checking for the validation simulation and analysis of the fast. dynamic casting algorithm Due to the heavy computational overhead and the. state space explosion problem the application of formal verification techniques is. limited to abstract models of the system s design In this work we introduce and. apply an innovative expression template based technique for extracting semantic. information from the C source code in order to deliver a practical and verifiable. implementation of the G S fast dynamic casting scheme This paper makes the. following contributions, 1 Introduces the use of a co simulation framework based on model checking for. the analysis and improvement of a compiler heuristics optimization problem. 2 Verifies and analyzes the G S C fast dynamic casting scheme and its ap. plication in mission critical code such as the MDS Data Management Services. Journal of Computing Science and Engineering Vol 2 No 4 December 2008. 3 Implements optimizations to the G S heuristics leading to the discovery of. optimal type ID assignment in 85 of the class hierarchies in contrast to 48. for the original G S algorithm, 4 Presents the design and application of an innovative expression template based. approach for extracting semantic information from the application s source code. in order to guarantee a practical and verifiable implementation of the fast dy. namic casting scheme, The rest of the paper is organized as follows section 2 a brief description of. the G S fast dynamic cast algorithm section 3 our approach to co simulation. and improvements to the G S heuristics section 4 discussion on the challenges. of mission critical code and the applicability of the G S dynamic cast section 5. performance results for the G S algorithm and the proposed improvements section. 6 design and implementation of Basic Query a library for extracting semantic. information from C programs and its application for delivering a practical and. verifiable fast dynamic cast operation and section 7 conclusion. 2 FAST DYNAMIC CASTING ALGORITHM, The G S fast constant time implementation of the dynamic cast operator works. as follows at link time a static integer type ID number preferably 32 or 64 bit. long is assigned to each class The ID numbers are selected so that the operation. ida modulus idb yields zero if and only if the class with ida is derived from the. class with idb This is done by exploiting the uniqueness of factorization of integers. into prime factors Each class is assigned a key prime number The type ID of. a class is calculated by multiplying its key number with the key numbers of each. Journal of Computing Science and Engineering Vol 2 No 4 December 2008. of its base classes In the cases where a class contains more than a single copy of. a base class the type ID is computed by taking the square of the corresponding. base class ID The only constraint of the approach is the desire to limit the ID. size to fit the machine s built in integer types The key primes are not required to. be unique and the same prime key can be used for classes that belong to different. groups i e do not share common descendants Gibbs and Stroustrup suggest four. approaches for assigning the type IDs in a space efficient manner Each method is. based on a preliminary computation of the priority factor of each class The priority. reflects the class impact on the growth of the type ID numbers in the hierarchy. Thus classes with greater number of descendants should receive higher priority and. smaller key prime number values respectively The four possible schemes suggest. 1 The priority of a class is the maximum number of ancestors that any of its. descendants has This scheme was chosen for the initial implementation and. testing of the G S algorithm and also closely followed in the implementation of. the abstract model used for our simulation, 2 3 4 If a range of primes is assigned to every level with wider levels receiving.
larger initial values then each node could be assigned an additional value that. is proportional to the logarithm of the 2 minimum 3 mean 4 maximum. prime in its level Priorities of hierarchy leaves are computed by taking the sum. of these additional values for the leaf itself and all of its ancestor classes. After the priority of each class has been computed the classes with the highest. priority get the smallest prime numbers According to this scheme prime numbers. Journal of Computing Science and Engineering Vol 2 No 4 December 2008. can be reused only if there are two classes on the same level of the class hierarchy. and only if they do not share common descendants they are not siblings and. also that none of their parents share a common descendant According to the ID. Fig 1 A class hierarchy with 11 classes,assignment rules we know that. 1 idx kx ka 2 ka1 kb 2 kb1 kc,2 idy ky kc kc1 kd 2 kd1 kb. 3 idz kz kd kd1 kc, As an example let us consider the class hierarchy presented in Figure 1 Given a. set Sclasses with 11 classes in the hierarchy and the set of the first 11 prime numbers. P 2 3 5 7 11 13 17 19 23 29 31 we must assign each class V a key kv P. such that the maximum of the set idleaf idx idy idz the set consisting of the. ID numbers of all leaf nodes in Sclasses is minimal As we already know prime. numbers need not be unique for each class and can be reused in same circumstances. 3 A CO SIMULATION FRAMEWORK, The goals of the co simulation framework are to validate the main invariants of the. G S heuristics improve its performance and establish its applicability in mission. critical systems The co simulation process in the framework Figure 2 consists. of three consecutive stages verification evaluation and analysis The verification. Journal of Computing Science and Engineering Vol 2 No 4 December 2008. phase is a straightforward application of model checking where an abstract descrip. tion of the system s behavior is checked against a set of invariants In the evaluation. stage the simulation results from the probabilistic approach are contrasted to the. outcome of the deterministic approach The aim of the analysis stage is to closely. examine the instances where the solutions yielded by the two implementations dif. fer We identify patterns among the inconsistent results that reveal the weaknesses. of the probabilistic solution The framework works by executing two independent. Fig 2 A Co Simulation Framework for G S Improvement and Verification. models the G S model and the exhaustive search model The first input compo. nent to the co simulation framework Figure 2 is an abstract model of the G S fast. dynamic casting heuristics implemented in Promela SPIN s input language and. the embedded C primitives it allows The G S abstract model is subsequently used. to verify the main invariants of the G S heuristics and at the same time provide. us with a simulation testbed to examine the heuristics performance The second. component of the framework is the exhaustive search model that simply looks into. all possible type ID assignments to discover the optimal solution for a given class. Journal of Computing Science and Engineering Vol 2 No 4 December 2008. hierarchy We employ SPIN s search engine to perform the exhaustive search In. Algorithm 1 we present the pseudocode of our co simulation approach The fol. lowing sections elaborate in more details on each of the stages of the framework. Algorithm 1 Pseudocode of the co simulation approach. 1 const int M AX N U M BER T EST S,2 V ERIF Y,4 F ormal V erif ication G S M odel error report.
5 if no errors then,6 goto EV ALU AT E,8 study counter example. 9 correct G S,10 until T RU E,11 EV ALU AT E,12 count 0. 13 for count M AX N U M BER T EST S do,14 Simulation G S M odel G S solution. 15 Enumeration Exhaustive Search M odel best solution. 16 if G S solution 6 best solution then,17 add instance to SIS. 19 AN ALY ZE,20 for all i SIS do,21 look f or a pattern.
22 modif y G S,23 goto EV ALU AT E,3 1 Formal Verification. Every G S implementation operates under the assumption that when a prime num. ber is reused it is assigned to non conflicting classes In addition the maximum. type ID must fit within the boundaries of a memory word We check these invari. ants during the program verification phase Establishing the validity of the G S. invariants is done by straightforward application of model checking with SPIN In. SPIN the critical system properties are expressed in the syntax of linear time logic. Based on the G S abstract specification the model checker performs a systematic. Journal of Computing Science and Engineering Vol 2 No 4 December 2008. exploration of all possible states In case of failure SPIN provides a counterexam. ple that demonstrates a behavior that has led to an illegal state In our model the. invariants are expressed as a never claim Holzmann 2003 and are checked just. before and after the execution of every statement,3 2 Evaluation. SPIN has been previously employed to implement solutions of scheduling Brinksma. and Mader 2000 and discrete optimization Ruys 2003 problems The problem we. face in the G S heuristics is a combinatorial optimization problem Nemhauser and. Wolsey 1988 Given a finite set I a collection F of subsets of I and a real valued. function w defined on I a discrete optimization problem could be defined as the. task of finding a member S of F such that w e is as small or as large as. Except for the simplest cases a discrete optimization problem is difficult because. its design space is typically disjoint and nonconvex Therefore the optimization. methods applied to continuous optimization problems cannot be utilized in this. case In a small discrete problem it would be possible to exhaustively list all possi. ble combinations As the number of parameters increase the state explosion makes. optimizations difficult The two general strategies for approaching a discrete opti. mization problem can be classified as deterministic and probabilistic What we do. for the G S exploration in SPIN could be described as applying a deterministic. approach for the evaluation of a set of proposed probabilistic methods The Branch. and Bound method Nemhauser and Wolsey 1988 guarantees the discovery of the. global optimum in the cases when the problem is linear or convex and is the most. Journal of Computing Science and Engineering Vol 2 No 4 December 2008. frequently used discrete optimization method It is based on the sequential analysis. of the discrete tree of each parameter The branches that can be estimated to reach. invalid or unfeasible solutions are consequently eliminated This simple optimiza. tion could also be applied in some limited cases in the SPIN s Fast Dynamic Casting. exhaustive search Let us explore a class hierarchy with three classes A B and. C where B is derived from A and C is derived from both A and B In this case. we have Sclasses A B C P 2 3 5 and idleaf idc The enumeration. is given in Table I We assume that the computation starts at a state S0 where. idc kc kb ka 2 ka kb kc,Table I Enumeration of all solutions. all three keys ka kb and kc are uninitialized Then we assign possible values from. the set P to the key variables of the classes A B and C The enumeration shown. above can be expressed as the computation shown on Figure 3 The graph shows. Fig 3 Exhaustive search computation, only the valid states of the computation There are a number of invalid states that. Journal of Computing Science and Engineering Vol 2 No 4 December 2008. are not shown on the graph For example according to the rules defined in G S. it is possible to reuse some of the prime numbers in P Thus we can try and add. an edge kb 2 in state S1 however the reuse of 2 in this case is invalid since A. and B are conflicting classes, The illustrated automation in Figure 3 provides a foundation for the construction.
of a Promela model for the deterministic solution Each possible prime number. assignment to a given class key is represented by a separate state transition in. the exhaustive search model SPIN initiates the optimum search at state S0 and. visits all possible states At each end state the value of the minimum of the set. of leaves in this case represented only by idc is computed and compared to the. current minimum This approach is similar to the algorithm described by Ruys. in Ruys 2003 and shown in Algorithm 2 For such an application we use the. model checker in a somewhat unusual fashion In this scenario the validation. property checks whether the value of idc is greater than the current minimum Each. time this condition is violated the current minimum is updated and the process is. automatically repeated until SPIN confirms that there are no routes violating the. specification Since the solution is deterministic it is guaranteed to discover the. Algorithm 2 Finding the global minimum in the state space. 1 intput P romela model M,2 output the optimal minimum f or the problem M. 3 min worst case maximum value f or id,5 use SP IN to check M with condition idc min. 6 if error f ound then,8 until error f ound, global optimum for type ID assignment The performance of the G S heuristics. Journal of Computing Science and Engineering Vol 2 No 4 December 2008. is measured by running a simulation of the G S model that has been used earlier. for verification Now we are left with only one important task not automated at. this stage the comparison of the results from the probabilistic and deterministic. solutions Once we identify a set of inconsistent results we try to find a pattern. and refine the G S heuristics Then the refined scheme is implemented in the. probabilistic model and the evaluation process is reiterated. 3 3 Analysis, The simulation and enumeration models are continuously executed until if possible. a set of instances with inconsistent solutions can be identified Thus each instance. in the Set of Inconsistent Solutions SIS represents a given class hierarchy for. which the deterministic and probabilistic approach have discovered different solu. tions The class hierarchies for each test could be guided or created in a random. fashion For the generation of the test data in our experiments we implemented. a pseudo random class hierarchy generation algorithm in a manner similar to the. TGFF Task Graphs For Free method as described in Dick et al 1998 We look. for patterns among the collected hierarchies in SIS and seek clues that can lead us. to improvements of the G S scheme Potential improvements are tested by adding. them to the G S model and evaluate their effect Such scheme modifications are. carefully selected since it is possible that they might enhance a given G S feature. and at the same time weaken another Ideally the improvements lead to a heuristic. scheme that provides the best solutions for a larger number of the test hierarchies. and at the same time has a time complexity equal to or less than the earlier heuristic. Journal of Computing Science and Engineering Vol 2 No 4 December 2008.

Related Books

Environmental, Social and Governance (ESG)

Environmental Social and Governance ESG

Source: The Hollywood Reporter 2018 Source: The New York Times 2018 2. Connectivity and reputation3. Opportunity to innovate4. Intangible assets & investor interest While the public is becoming more ethically and environmentally conscious

OUTDOOR POWER EQUIPMENT - HORS BORD YAMAHA

OUTDOOR POWER EQUIPMENT HORS BORD YAMAHA

The starting requirements of devices utilizing electric motors, for example an air compressor, a sump pump, etc., may be significantly higher than the actual wattage required during continuous operation. This must be considered when estimating your power needs. Most small universal motors such as drills, small saws, blenders, etc., require some additional current during start-up. In most cases ...

Surrey Art Gallery

Surrey Art Gallery

SAGA: Heart to Home Market ... continuity, and creative expression to support the ... in the garage, and bundle up that treasured item.

McSweeny Elementary School

McSweeny Elementary School

DAILY SCHEDULES See Bell Schedule CALENDAR DATES See School Calendar PROCEDURES / POLICIES AFTER SCHOOL PROGRAM (SAFE) - The District offers a program for after school care from 2:14-6:00 pm. For more information, please call (951) 765-5100 ext. 3901 ATTENDANCE PROCEDURES IT IS THE STRONG BELIEF OF THE HEMET UNIFIED SCHOOL

assets.matchbin.com

assets matchbin com

Friday Prime Time, November 14 4 P.M. 4:30 5 P.M. 5:30 6 P.M. 6:30 7 P.M. 7:30 8 P.M. 8:30 9 P.M. 9:30 10 P.M. 10:30 11 P.M. 11:30 BASIC CABLE KUTV 2 Oprah Winfrey b ...

Section 6 Troubleshooting - emanuals.nordson.com

Section 6 Troubleshooting emanuals nordson com

Section 6 Troubleshooting WARNING: ... Refer to Section 5, Relieving System Pressure. Refer to the safety information provided with optional equipment. If the melter is removed from its sub-base for diagnostic checks or service, ensure that the ground lead between the chassis and the sub-base is re-attached when the melter is reconnected to the sub-base. 6-2 Troubleshooting Part 1024496D 2006 ...

Section 6 Troubleshooting

Section 6 Troubleshooting

Refer to Section 5, Relieving System Pressure. Refer to the safety information provided with optional equipment. If the melter is removed from its sub-base for diagnostic checks or service, ensure that the ground lead between the chassis and the sub-base is re-attached when the melter is reconnected to the sub-base. 6-2 Troubleshooting Part 1024496C Manual 41-PROBLUE-MA-01 2004 Nordson ...

Product Launch Case Studies 2008 - 3dB Creative

Product Launch Case Studies 2008 3dB Creative

Following is an outline of the product launch process at 3dB Creative, ... to create a graffiti-style take ... This innovative hardware / software bundle served to ...

KDUMP AND INTRODUCTION TO VMCORE ANALYSIS

KDUMP AND INTRODUCTION TO VMCORE ANALYSIS

KDUMP AND INTRODUCTION TO VMCORE ANALYSIS HOW TO GET STARTED WITH INSPECTING KERNEL FAILURES PATRICK LADD TECHNICAL ACCOUNT MANAGER, RED HAT ... Which is closely followed by a backtrace and what looks like a ... It requires a similar release system such as Red Hat Enterprise Linux 6 for vmcores captured on a Red Hat Enterprise Linux 6 system.

Linux Kernel GDB tracepoint module (KGTP)

Linux Kernel GDB tracepoint module KGTP

Linux kernel do single step Backtrace GDB can print backtrace of all stack frames with command "backtrace". KGTP can do it too.Howto backtrace (stack dump) Watchpoint GDB can let programe stop when some memory access happen with watchpoint. KGTP can record the memory access with