Static analysis for detecting high-level races in RTOS kernels

Author(s):  
Rekha Pai ◽  
Abhishek Singh ◽  
Deepak D’Souza ◽  
Meenakshi D’Souza ◽  
Prathibha Prakash
Keyword(s):  
2004 ◽  
Vol 11 (33) ◽  
Author(s):  
Aske Simon Christensen ◽  
Christian Kirkegaard ◽  
Anders Møller

We show that it is possible to extend a general-purpose programming language with a convenient high-level data-type for manipulating XML documents while permitting (1) precise static analysis for guaranteeing validity of the constructed XML documents relative to the given DTD schemas, and (2) a runtime system where the operations can be performed efficiently. The system, named Xact, is based on a notion of immutable XML templates and uses XPath for deconstructing documents. A companion paper presents the program analysis; this paper focuses on the efficient runtime representation.


2014 ◽  
Vol 580-583 ◽  
pp. 2924-2927 ◽  
Author(s):  
Pavel A. Akimov ◽  
Mojtaba Aslami

This paper is devoted to correct and efficient method of local static analysis of Bernoulli beam on elastic foundation. First of all, problem discretized by finite difference method, and then transformed to a localized one by using the Haar wavelets. Finally, imposing an optimal reduction in wavelet coefficients, the localized, reduced results can be obtained. It becomes clear after comparison with analytical solutions, that the localization of the problem by multiresolution wavelet approach gives exact solution in desired regions of beam even in high level of reduction in wavelet coefficients. This localization can be applied to any arbitrary region of the beam by choosing optimum reduction matrix and obtaining exact solutions with an acceptable reduced size of the problem.


2013 ◽  
Vol 81 (3) ◽  
Author(s):  
Zheng Jiexin ◽  
Andrew Palmer ◽  
Paul Brunning

A pipeline on the seabed may be struck by moving trawl gear, and that may damage the pipeline. Trenching can be a useful but expensive way to protect the pipeline. Pipe-in-pipe and bundled pipeline systems are widely used in the offshore industry recently because of their high level of thermal insulation and because they lend themselves to rapid and economical installation. However, there is no clearly specified standard method to analyze the overtrawlability of pipe-in-pipe systems. If we apply the same method as for the single wall pipe, it is likely to result in a conservative design for the pipe-in-pipe. The objective of this paper is to investigate the overtrawlability of pipe-in-pipe, especially in the impact phase, and to fill this gap. In this study, the authors demonstrate that a quasi-static analysis can replace a dynamic analysis to some extent because the overall response does not show a big difference. The demonstration is based on both quasi-static indentation tests and impact tests for single wall pipe and pipe-in-pipe, as well as the corresponding finite element (FE) models. The FE models not only help to compare the responses but also offer a way to analyze the overtrawlability of the pipe-in-pipe. The quasi-static FE models are used for a further comparison between a pipe-in-pipe and a 406.4 mm (16 in.) single wall pipe to illustrate the overtrawlability of the pipe-in-pipe.


Author(s):  
MIGUEL A. SANCHEZ-ORDAZ ◽  
ISABEL GARCIA-CONTRERAS ◽  
VICTOR PEREZ ◽  
JOSÉ F. MORALES ◽  
PEDRO LOPEZ-GARCIA ◽  
...  

Abstract Assertion checking is an invaluable programmer’s tool for finding many classes of errors or verifying their absence in dynamic languages such as Prolog. For Prolog programmers, this means being able to have relevant properties, such as modes, types, determinacy, nonfailure, sharing, constraints, and cost, checked and errors flagged without having to actually run the program. Such global static analysis tools are arguably most useful the earlier they are used in the software development cycle, and fast response times are essential for interactive use. Triggering a full and precise semantic analysis of a software project every time a change is made can be prohibitively expensive. This is specially the case when complex properties need to be inferred for large, realistic code bases. In our static analysis and verification framework, this challenge is addressed through a combination of modular and incremental (context- and path-sensitive) analysis that is responsive to program edits, at different levels of granularity. In this tool paper, we present how the combination of this framework within an integrated development environment (IDE) takes advantage of such incrementality to achieve a high level of reactivity when reflecting analysis and verification results back as colorings and tooltips directly on the program text – the tool’s VeriFly mode. The concrete implementation that we describe is Emacs-based and reuses in part off-the-shelf “on-the-fly” syntax checking facilities (flycheck). We believe that similar extensions are also reproducible with low effort in other mature development environments. Our initial experience with the tool shows quite promising results, with low latency times that provide early, continuous, and precise assertion checking and other semantic feedback to programmers during the development process. The tool supports Prolog natively, as well as other languages by semantic transformation into Horn clauses.


2003 ◽  
Vol 10 (19) ◽  
Author(s):  
Christian Kirkegaard ◽  
Anders Møller ◽  
Michael I. Schwartzbach

XML documents generated dynamically by programs are typically represented as text strings or DOM trees. This is a low-level approach for several reasons: 1) Traversing and modifying such structures can be tedious and error prone; 2) Although schema languages, e.g. DTD, allow classes of XML documents to be defined, there are generally no automatic mechanisms for statically checking that a program transforms from one class to another as intended. We introduce X<small>ACT</small>, a high-level approach for Java using XML templates as a first-class data type with operations for manipulating XML values based on XPath. In addition to an efficient runtime representation, the data type permits static type checking using DTD schemas as types. By specifying schemas for the input and output of a program, our algorithm will statically verify that valid input data is always transformed into valid output data and that no errors occur during processing.


2003 ◽  
Vol 10 (29) ◽  
Author(s):  
Aske Simon Christensen ◽  
Christian Kirkegaard ◽  
Anders Møller

We show that it is possible to extend a general-purpose programming language with a convenient high-level data-type for manipulating XML documents while permitting (1) precise static analysis for guaranteeing validity of the constructed XML documents relative to the given DTD schemas, and (2) a runtime system where the operations can be performed efficiently. The system, named X<small>ACT</small>, is based on a notion of immutable XML templates and uses XPath for deconstructing documents. A companion paper presents the program analysis; this paper focuses on the efficient runtime representation.


2011 ◽  
Vol 8 (2) ◽  
pp. 534-548 ◽  
Author(s):  
João Lourenço ◽  
Diogo Sousa ◽  
Bruno Teixeira ◽  
Ricardo Dias

Concurrent programs may suffer from concurrency anomalies that may lead to erroneous and unpredictable program behaviors. To ensure program correctness, these anomalies must be diagnosed and corrected. This paper addresses the detection of both low- and high-level anomalies in the Transactional Memory setting. We propose a static analysis procedure and a framework to address Transactional Memory anomalies. We start by dealing with the classic case of low-level dataraces, identifying concurrent accesses to shared memory cells that are not protected within the scope of a memory transaction. Then, we address the case of high-level dataraces, bringing the programmer?s attention to pairs of memory transactions that were misspecified and should have been combined into a single transaction. Our framework was applied to a set of programs, collected form different sources, containing well known low- and high-level anomalies. The framework demonstrated to be accurate, confirming the effectiveness of using static analysis techniques to precisely identify concurrency anomalies in Transactional Memory programs.


2021 ◽  
Vol 6 (2) ◽  
pp. 111
Author(s):  
Rinaldi Alamsyah ◽  
Indra Noer Hamdhan

ABSTRAKWilayah perkotaan yang didalamnya terdapat perkantoran dan tempat yang memiliki tingkat kegiatan yang sangat tinggi, menjadikan struktur terowongan bawah tanah sebagai salah satu solusi untuk meningkatkan infrastruktur transportasi secara  optimal. Terowongan kereta cepat Indonesia merupakan salah satu terowongan yang dibangun dan berlokasi di Halim, DKI Jakarta. Terowongan dengan panjang 1.885 m ini memiliki jalur ganda (Double Track Railway). Untuk mengetahui stabilitas dan deformasi terowongan pada saat konstuksi, dilakukan analisis geoteknik. Analisis yang dilakukan yaitu analisis statik dan kondisi longterm dengan analisis dinamik. Tunneling Bore Machine (TBM) dengan sistem perkuatan linning precast dan grouting dipilih sebagai metode konstruksi untuk membangun terowongan. Pemodelan analisis statik menghasilkan deformasi terbesar 0,03056 m dan nilai faktor keamanan 1,869.Kata kunci: terowongan kereta cepat Indonesia, stabilitas, deformasi, faktor keamanan, TBM, PLAXIS 3D, linning, grouting ABSTRACTUrban areas with offices and places that have a very high level of activity make underground tunnel structures one of the solutions to optimally improve transportation infrastructure. The Indonesian fast train tunnel is one of the tunnels built and located at Halim, DKI Jakarta. The tunnel with a length of 1,885 m has a double track (Double Track Railway). To determine the stability and deformation of the tunnel during construction, a geotechnical analysis was performed. The analysis performed is static analysis and longterm conditions with dynamic analysis. Tunneling Bore Machine (TBM) with precast linning reinforcement and grouting system was chosen as the construction method for tunneling. Static analysis modeling produces the largest deformation 0.03056 m and a safety factor value of 1.869.Keywords: tunnel, face stability, deformation, safety factor, TBM, numerical method, PLAXIS 3D, linning, grouting


2018 ◽  
Vol 14 (25) ◽  
pp. 1-11
Author(s):  
Mood Venkanna ◽  
Rameshwar Rao

Introduction: The application of specific instructions significantly improves energy, performance, and code size of configurable processors. The design of these instructions is performed by the conversion of patterns related to application-specific operations into effective complex instructions. This research was presented at the icitkm Conference, University of Delhi, India in 2017.Methods: Static analysis was a prominent research method during late the 1980’s. However, end-to-end measurements consist of a standard approach in industrial settings. Both static analysis tools perform at a high-level in order to determine the program structure, which works on source code, or is executable in a disassembled binary. It is possible to work at a low-level if the real hardware timing information for the executable task has the desired features.Results: We experimented, tested and evaluated using a H.264 encoder application that uses nine cis, covering most of the computation intensive kernels. Multimedia applications are frequently subject to hard real time constraints in the field of computer vision. The H.264 encoder consists of complicated control flow with more number of decisions and nested loops. The parameters evaluated were different numbers of A partitions (300 slices on a Xilinx Virtex 7each), reconfiguration bandwidths, as well as relations of cpu frequency and fabric frequency fCPU/ffabric. ffabric remains constant at 100MHz, and we selected a multiplicity of its values for fCPU that resemble realistic units. Note that while we anticipate the wcet in seconds (wcetcycles/ f CPU) to be lower (better) with higher fCPU, the wcet cycles increase (at a constant ffabric) because hardware cis perform less computations on the reconfigurable fabric within one cpu cycle.Conclusions: The method is similar to tree hybridization and path-based methods which are less precise, and to the global ipet method, which is more precise. Optimization is evaluated with the Discrete Particle Swarm Optimization (dpso) algorithm for wcet. For several real-world applications involving embedded processors, the proposed technique develops improved instruction sets in comparison to native instruction sets.Originality: For wcet estimation, flow analysis, low-level analysis and calculation phases of the program need to be considered. Flow analysis phase or the high-level of analysis helps to extract the program’s dynamic behavior that gives information on functions being called, number of loop iteration, dependencies among if-statements, etc. This is due to the fact that the analysis is unaware of the execution path corresponding to the longest execution time.Limitations: This path is executed within a kernel iteration that relies upon the nature of mb, either i-mb or p-mb, determined by the motion estimation kernel, that is, its’ input depends on the i-mb and p-mb paths ,which also contain separate cis leading to the instability of the worst-case path, that is, adding more partitions to the current worst-case path can result in the other path becoming the worst case. The pipeline stalls for the reconfiguration delay and continues when entering the kernel once the reconfiguration process finishes.


Author(s):  
Abhishek Singh ◽  
Rekha Pai ◽  
Deepak D’Souza ◽  
Meenakshi D’Souza
Keyword(s):  

Sign in / Sign up

Export Citation Format

Share Document