Dissertations / Theses on the topic 'Execution Time estimation'

Safety-critical systems - such as electronic flight control systems and nuclear reactor controls - must satisfy strict safety requirements. We are interested here in the application of formal methods - built upon solid mathematical bases - to verify the behavior of safety-critical systems. More specifically, we formally specify our algorithms and then prove them correct using the Coq proof assistant - a program capable of mechanically checking the correctness of our proofs, providing a very high degree of confidence. In this thesis, we apply formal methods to obtain safe Worst-Case Execution Time (WCET) estimations for C programs. The WCET is an important property related to the safety of critical systems, but its estimation requires sophisticated techniques. To guarantee the absence of errors during WCET estimation, we have formally verified a WCET estimation technique based on the combination of two main methods: a loop bound estimation and the WCET estimation via the Implicit Path Enumeration Technique (IPET). The loop bound estimation itself is decomposed in three steps: a program slicing, a value analysis based on abstract interpretation, and a loop bound calculation stage. Each stage has a chapter dedicated to its formal verification. The entire development has been integrated into the formally verified C compiler CompCert. We prove that the final estimation is correct and we evaluate its performances on a set of reference benchmarks. The contributions of this thesis include (a) the formalization of the techniques used to estimate the WCET, (b) the estimation tool itself (obtained from the formalization), and (c) the experimental evaluation. We conclude that our formally verified development obtains interesting results in terms of precision, but it requires special precautions to ensure the proof effort remains manageable. The parallel development of specifications and proofs is essential to this end. Future works include the formalization of hardware cost models, as well as the development of more sophisticated analyses to improve the precision of the estimated WCET.

Les systèmes informatiques critiques - tels que les commandes de vol électroniques et le contrôle des centrales nucléaires - doivent répondre à des exigences strictes en termes de sûreté de fonctionnement. Nous nous intéressons ici à l'application de méthodes formelles - ancrées sur de solides bases mathématiques - pour la vérification du comportement des logiciels critiques. Plus particulièrement, nous spécifions formellement nos algorithmes et nous les prouvons corrects, à l'aide de l'assistant à la preuve Coq - un logiciel qui vérifie mécaniquement la correction des preuves effectuées et qui apporte un degré de confiance très élevé. Nous appliquons ici des méthodes formelles à l'estimation du Temps d'Exécution au Pire Cas (plus connu par son abréviation en anglais, WCET) de programmes C. Le WCET est une propriété importante pour la sûreté de fonctionnement des systèmes critiques, mais son estimation exige des analyses sophistiquées. Pour garantir l'absence d'erreurs lors de ces analyses, nous avons formellement vérifié une méthode d'estimation du WCET fondée sur la combinaison de deux techniques principales: une estimation de bornes de boucles et une estimation du WCET via la méthode IPET (Implicit Path Enumeration Technique). L'estimation de bornes de boucles est elle-même décomposée en trois étapes : un découpage de programmes, une analyse de valeurs opérant par interprétation abstraite, et une méthode de calcul de bornes. Chacune de ces étapes est formellement vérifiée dans un chapitre qui lui est dédiée. Le développement a été intégré au compilateur C formellement vérifié CompCert. Nous prouvons que le résultat de l'estimation est correct et nous évaluons ses performances dans des ensembles de benchmarks de référence dans le domaine. Les contributions de cette thèse incluent la formalisation des techniques utilisées pour estimer le WCET, l'outil d'estimation lui-même (obtenu à partir de la formalisation), et l'évaluation expérimentale des résultats. Nous concluons que le développement fondé sur les méthodes formelles permet d'obtenir des résultats intéressants en termes de précision, mais il exige des précautions particulières pour s'assurer que l'effort de preuve reste maîtrisable. Le développement en parallèle des spécifications et des preuves est essentiel à cette fin. Les travaux futurs incluent la formalisation de modèles de coût matériel, ainsi que le développement d'analyses plus sophistiquées pour augmenter la précision du WCET estimé
Safety-critical systems - such as electronic flight control systems and nuclear reactor controls - must satisfy strict safety requirements. We are interested here in the application of formal methods - built upon solid mathematical bases - to verify the behavior of safety-critical systems. More specifically, we formally specify our algorithms and then prove them correct using the Coq proof assistant - a program capable of mechanically checking the correctness of our proofs, providing a very high degree of confidence. In this thesis, we apply formal methods to obtain safe Worst-Case Execution Time (WCET) estimations for C programs. The WCET is an important property related to the safety of critical systems, but its estimation requires sophisticated techniques. To guarantee the absence of errors during WCET estimation, we have formally verified a WCET estimation technique based on the combination of two main methods: a loop bound estimation and the WCET estimation via the Implicit Path Enumeration Technique (IPET). The loop bound estimation itself is decomposed in three steps: a program slicing, a value analysis based on abstract interpretation, and a loop bound calculation stage. Each stage has a chapter dedicated to its formal verification. The entire development has been integrated into the formally verified C compiler CompCert. We prove that the final estimation is correct and we evaluate its performances on a set of reference benchmarks. The contributions of this thesis include (a) the formalization of the techniques used to estimate the WCET, (b) the estimation tool itself (obtained from the formalization), and (c) the experimental evaluation. We conclude that our formally verified development obtains interesting results in terms of precision, but it requires special precautions to ensure the proof effort remains manageable. The parallel development of specifications and proofs is essential to this end. Future works include the formalization of hardware cost models, as well as the development of more sophisticated analyses to improve the precision of the estimated WCET

Made available in DSpace on 2014-06-12T15:52:55Z (GMT). No. of bitstreams: 1 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009
Nos últimos anos, a redução do consumo de energia das aplicações dos sistemas embarcados tem recebido uma grande atenção da comunidade científica, visto que, como o tempo de resposta e o baixo consumo de energia são requisitos conflitantes, esses estudos tornam-se altamente necessários. Nesse contexto, é proposta uma metodologia aplicada nas fases iniciais de projeto para dar suporte às decisões relativas ao consumo de energia e ao desempenho das aplicações desses dispositivos embarcados. Al´em disso, esse trabalho propõe modelos temporizados de eventos discretos que são avaliados através de uma metodologia de simulção estocástica com o objetivo de representar diferentes cenários dos sistemas com facilidade. Dessa forma, para cada cenário ´e preciso decidir o n´umero máximo de simulações e o tamanho de cada rodada da simulação, onde ambos os fatores podem impactar no desempenho para se obter tais estimativas. Essa metodologia considera também, um modelo intermediário que representa a descrição do comportamento do sistema e, é através desse modelo que cenários são analisados. Esse modelo intermediário ´e baseado em redes de Petri coloridas temporizadas que permitem não somente a anáise do software, mas também fornece suporte a um conjunto de métodos bem estabelecidos para verificações de propriedades. É nesse contexto que o software, ALUPAS, responsável por estimar o consumo de energia e o tempo de execução dos sistemas embarcados é apresentado. Por fim, um caso de estudo real, assim como tamb´em, exemplos customizados são apresentados com a finalidade de mostrar a aplicabilidade desse trabalho, onde usuários não especializados não precisam interagir diretamente com o formalismo de redes de Petri.

Execution time estimation plays an important role in computer system design. It is particularly critical in real-time system design, where to meet a deadline can be as important as to ensure the logical correctness of a program. To accurately estimate the execution time of a program can be extremely challenging, since the execution time of a program varies with inputs, the underlying computer architectures, and run-time dynamics, among other factors. The problem becomes even more challenging as computing systems moving from single core to multi-core platforms, with more hardware resources shared by multiple processing cores. The goal of this research is to investigate the relationship between the execution time of a program and the underlying architecture features (e.g. cache size, associativity, memory latency), as well as its run-time characteristics (e.g. cache miss ratios), and based on which, to estimate its execution time on a multi-core platform based on a regression approach. We developed our test platform based on GEM5, an open-source multi-core cycle-accurate simulation tool set. Our experimental results show clearly the strong relationship of the program execution time to architecture features and run-time characteristics. Moreover, we developed different execution time estimation algorithms using the regression approach for different programs with different software characteristics to improve the estimation accuracy.

Immersive applications, such as computer gaming, computer vision and video codecs, are an important emerging class of applications with QoS requirements that are difficult to characterize and control using traditional methods. This thesis proposes new techniques reliant on execution-time variance to both characterize and control program behavior. The proposed techniques are intended to be broadly applicable to a wide variety of immersive applications and are intended to be easy for programmers to apply without needing to gain specialized expertise. First, we create new QoS controllers that programmers can easily apply to their applications to achieve desired application-specific QoS objectives on any platform or application data-set, provided the programmers verify that their applications satisfy some simple domain requirements specific to immersive applications. The controllers adjust programmer-identified knobs every application frame to effect desired values for programmer-identified QoS metrics. The control techniques are novel in that they do not require the user to provide any kind of application behavior models, and are effective for immersive applications that defy the traditional requirements for feedback controller construction. Second, we create new profiling techniques that provide visibility into the behavior of a large complex application, inferring behavior relationships across application components based on the execution-time variance observed at all levels of granularity of the application functionality. Additionally for immersive applications, some of the most important QoS requirements relate to managing the execution-time variance of key application components, for example, the frame-rate. The profiling techniques not only identify and summarize behavior directly relevant to the QoS aspects related to timing, but also indirectly reveal non-timing related properties of behavior, such as the identification of components that are sensitive to data, or those whose behavior changes based on the call-context.

Testing plays a vital role in the software development life cycle by verifying and validating the software's quality. Since software testing is considered as an expensive activity and due to thelimitations of budget and resources, it is necessary to know the execution time of the test cases for an efficient planning of test-related activities such as test scheduling, prioritizing test cases and monitoring the test progress. In this thesis, an approach is proposed to predict and estimate the execution time of manual test cases written in English natural language. The method uses test specifications and historical data that are available from previously executed test cases. Our approach works by obtaining timing information from each and every step of previously executed test cases. The collected data is used to estimate the execution time for non-executed test cases by mapping them using text from their test specifications. Using natural language processing, texts are extracted from the test specification document and mapped with the obtained timing information. After estimating the time from this mapping, a linear regression analysis is used to predict the execution time of non-executed test cases. A case study has been conducted in Bombardier Transportation (BT) where the proposed method is implemented and the results are validated. The obtained results show that the predicted execution time of studied test cases are close to their actual execution time.

On utilise un graphe pour représenter les relations entre les différentes tâches constituant chaque algorithme d'identification et de commande. Ce graphe sert à l'ordonnancement et au calcul de la durée d'exécution grâce à la méthode CPM (critical path method)

碩士
國立成功大學
資訊工程學系
102
With the development of GPU, there are hundreds of cores on one GPU which is much more than a four-core or eight-core CPU. It starts new direction of high speed computing. GPU computing’s performance is much better than before. Cloud computing also developed rapidly, MapReduce [1] on GPU clusters can execute graphic processing or general purpose application even much faster. For developers, it is a new challenge. When they are writing new applications on GPU clusters, they have to manage the resources and parameters on GPU device. It will cost a lot of time on tuning performance [2] studying the details of MapReduce and GPU computing or finding the bottleneck of programs. In this thesis, the execution details of MapReduce on GPU clusters is discussed precisely. We used Stochastic Petri Net [4] to analyze the influence of GPU computing and develop SPN-GC model. The model defines formulas of every stage’s execution time and respond the estimation execution time under different input data size immediately. It will help the developer to find out the time bottleneck. The result of experiment shows out the comparison between the estimation execution time and actual test under different input data size. The error range is found out to be within 10%, and it can be a reference when developer is tuning the program.

碩士
國立中正大學
資訊工程研究所
101
With the machine tool industry due to intense competition at home and abroad to diversity and intellectual trend, gradually forming machine tools feature diverse, but the machine tool must meet the requirements of real-time systems. Real-time systems emphasize efficiency, rapid response, and reliability, making the hard real-time systems must meet safety and rigorous execution time limit, but also so hard real-time systems are widely used in the aerospace, automotive, and industrial machinery, such emphasis on timeliness field, but with many smart applications and increased functionality, basic motion control functions cause the system to be an increase in execution time, so that the system produces unpredictable consequences. The analysis of program execution time worst (worst-case execution time, WCET) can avoid unpredictable consequences arising. Therefore, in order to ensure the correctness of the system perform aging, this paper combines the advantages of existing real-time systems, to accelerate the execution speed of the machine tool system, and modify the well-known academics worst execution time prediction tool Chronos, the Chronos was originally for the MIPS architecture basis, by modifying the instruction set architecture (instruction set architecture) and micro-structure (microarchitecture), let Chronos able to predict the approximate Intel-based PC-Based motion Control machine Tools system maximum execution time of the program to the system to meet the system's final implementation period.

碩士
國立中正大學
資訊工程研究所
100
Developing high performance programs is the critical issue of programmers. Before releasing a program to the client, programmers will usually evaluate the performance of the program and exploit the compiler optimization options to improve the performance as much as possible. This thesis develops a program execution time estimation tool based on the compiler intermediate language - register transfer language. By using program static analysis, the estimation of the program execution time can be performed with as few program executions as possible. From the observation of a preliminary experiment on the comparison of the estimated execution time and the exertion time obtained from a simula- tor, the average accuracy rate of the estimated execution time is 72.03%, and the average accuracy rates are very consistent for different compiler optimization options. This thesis also utilizes this program execution time estimation tool to upgrade the speed of the iterative compilation. By using a control flow pattern caching mechanism, a preliminary experiment shows that this program execution time estimation tool can significantly upgrade the speed of the iterative compilation.

Estimating program worst case execution time (WCET) is an important problem in the domain of real-time systems and embedded systems that are deadline-centric. If WCET of a program is found to exceed the deadline, it is either recoded or the target architecture is modified to meet the deadline. Predominantly, there exist three broad approaches to estimate WCET- static WCET analysis, hybrid measurement based analysis and statistical WCET analysis. Though measurement based analyzers benefit from knowledge of run-time behavior, amount of instrumentation remains a concern. This thesis proposes a CPI-centric WCET analyzer that estimates WCET as a product of worst case instruction count (IC) estimated using static analysis and worst case cycles per instruction (CPI) computed using a function of measured CPI. In many programs, it is observed that IC and CPI values are correlated. Five different kinds of correlation are found. This correlation enables us to optimize WCET from the product of worst case IC and worst case CPI to a product of worst case IC and corresponding CPI. A prime advantage of viewing time in terms of CPI, enables us to make use of program phase behavior. In many programs, CPI varies in phases during execution. Within each phase, the variation is homogeneous and lies within a few percent of the mean. Coefficient of variation of CPI across phases is much greater than within a phase. Using this observation, we estimate program WCET in terms of its phases. Due to the nature of variation of CPI within a phase in such programs, we can use a simple probabilistic inequality- Chebyshev inequality, to compute bounds of CPI within a desired probability. In some programs that execute many paths depending on if-conditions, CPI variation is observed to be high. The thesis proposes a PC signature that is a low cost way of profiling path information which is used to isolate points of high CPI variation and divides a phase into smaller sub-phases of lower CPI variation. Chebyshev inequality is applied to sub-phases resulting in much tighter bounds. Provision to divide a phase into smaller sub-phases based on allowable variance of CPI within a sub-phase also exists. The proposed technique is implemented on simulators and on a native platform. Other advantages of phases in the context of timing analysis are also presented that include parallelized WCET analysis and estimation of remaining worst case execution time for a particular program run.

Preemptive Time Petri Nets (pTPNs) support modeling and analysis of concurrent timed software components running under fixed priority preemptive scheduling. The model is supported by a well established theory based on symbolic state-space analysis through Difference Bounds Matrix (DBM), with specific contributions on compositional modularization, trace analysis, and efficient over-approximation and clean-up in the management of suspension deriving from preemptive behavior. The aim of this dissertation is to devise and implement a framework that brings the theory to application. To this end, the theory is cast into an organic tailoring of design, coding, and testing activities within a V-Model software life cycle in respect of the principles of regulatory standards applied to the construction of safety-critical software components. To implement the toolchain subtended by the overall approach into a Model Driven Development (MDD) framework, the theory of state-space analysis is complemented with methods and techniques supporting semi-formal specification and automated compilation into pTPN models and real-time code, measurement-based Execution Time estimation, test-case selection and sensitization, coverage evaluation.