Understanding the execution time is critical for embedded, real-time applications. Worst-case execution time (WCET) is an important metric to check the real-time constraints imposed on embedded applications. For complex execution platforms, such as graphics processing units (GPUs), analysis of WCET imposes great challenges due to the complex characteristics of GPU architecture as well as GPU program semantics. In this paper, we propose GDivAn, a measurement-based WCET analysis tool for arbitrary GPU kernels. GDivAn systematically combines the strength of symbolic execution (SE) and genetic algorithm (GA) to maintain both the scalability and the effectiveness of the analysis process. Our evaluation with several open-source GPU kernels reveals the efficiency of GDivAn.

Today, the majority of control applications in embedded systems, e.g., in the automotive domain, are implemented as software tasks on shared platforms. Ignoring implementation impacts during the design of embedded control systems results in complex timing behaviors that may lead to poor performance and, in the worst case, instability of control applications. This article presents a methodology for implementation-aware design of high-quality and stable embedded control systems on shared platforms with complex timing behaviors.

The goal of this work is to facilitate the development of proactive power- and temperature-aware resource managers that leverage machine learning in order to attain their objectives. In this context, the availability of sufficiently large amounts of relevant data, which are essential for learning and, therefore, exploration of research ideas, is elusive. In order to fulfill the need, we present a toolchain for fast generation of realistic power and temperature profiles of computer systems. The toolchain provides profuse representative data to learn from during development stages. The overreaching objective is to help research by making it tractable to experiment with the highly promising but data-demanding state-of-the-art techniques for prediction.

In order to facilitate the development of intelligent resource managers of computer clusters, we investigate the utility of the state-of-the-art neural networks for the purpose of fine-grained long-range prediction of the resource usage in one such cluster. We consider a large data set of real-life traces and describe in detail our workflow, starting from making the data accessible for learning and finishing by predicting the resource usage of individual tasks multiple steps ahead. The experimental results indicate that such fine-grained traces as the ones considered possess a certain structure, and that this structure can be extracted by advanced machine-learning techniques and subsequently utilized for making informed predictions.

We present a framework for system-level analysis of electronic systems whose runtime behaviors depend on uncertain parameters. The proposed approach thrives on hierarchical interpolation guided by an advanced adaptation strategy, which makes the framework general and suitable for studying various metrics that are of interest to the designer. Examples of such metrics include the end-to-end delay, total energy consumption, and maximum temperature of the system under consideration. The framework delivers a light generative representation that allows for a straightforward, computationally efficient calculation of the probability distribution and accompanying statistics of the metric at hand. Our technique is illustrated by considering a number of uncertainty-quantification problems and comparing the corresponding results with exhaustive simulations.

Many modern applications exhibit a dynamic and nonstationary behavior, with certain characteristics in one phase of their execution, which change as the application enters new phases, in a manner unpredictable at design-time. In order to meet the demands of such applications, it is important to have adaptive and self-reconfiguring hardware platforms, coupled with intelligent on-line optimization algorithms, that together can adjust to the run-time requirements. Partially dynamically reconfigurable field programmable gate array architectures offer both high performance and flexibility. Despite these potential advantages, the challenges faced by designers trying to set-up a functioning system are still significant, mainly because of the still immature design tools and limited device drivers. We propose a complete framework, based on Xilinx’s commercial design suite, that enables an application designer to leverage the advantages of partial dynamic reconfiguration with minimal effort. Our IP-based architecture, together with the comprehensive application programming interface, can be employed to accelerate an application by dynamically scheduling hardware prefetches. Moreover, a piecewise linear predictor is used to capture correlations and predict the hardware modules that will generate the highest performance improvement. Our evaluation comprises of extensive simulations, as well as a complete implementation of the smallest univalue segment assimilating nucleus image processing application on the ML605 board from Xilinx. The measurements show a significant reduction of the expected execution time compared to previous state-of-the-art prefetching algorithms, with only a minor energy overhead.

Today, a considerable portion of embedded systems, e.g., automotive and avionic, comprise several control applications. Guaranteeing the stability of these control applications in embedded systems, or cyber-physical systems, is perhaps the most fundamental requirement while implementing such applications. This is different from the classical hard real-time systems where often the acceptance criterion is meeting the deadline. In other words, in the case of control applications, guaranteeing stability is considered to be a main design goal, which is linked to the amount of delay and jitter a control application can tolerate before instability. This advocates the need for new design and analysis techniques for embedded real-time systems running control applications. In this paper, the analysis and design of such systems considering a server-based resource reservation mechanism are addressed. The benefits of employing servers are manifold: providing a compositional and scalable framework, protection against other tasks misbehaviors, and systematic bandwidth assignment and co-design. We propose a methodology for designing bandwidth-optimal servers to stabilize control tasks. The pessimism involved in the proposed methodology is both discussed theoretically and evaluated experimentally.

We propose an analytical framework for probabilistic timing analysis of the event-triggered Dynamic segment of the FlexRay communication protocol. Specifically, our framework computes the Deadline Miss Ratio of each message. The core problem is formulated as a Mixed Integer Linear Program (MILP). Given the intractability of the problem, we also propose several techniques that help to mitigate the running times of our tool. This includes the re-engineering of the problem to run it on GPUs as well as reformulating the MILP itself.

Most importantly, we also show how our framework can handle correlations between the queuing events of messages. This is challenging because one cannot apply the convolution operator in the same way as in the case of independent queuing events.

We address the problem of automatically establishing correctness for programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. The programs we consider can make use of the shared variables to count and synchronize the spawned processes. This allows them to implement intricate synchronization mechanisms, such as barriers. Automatically verifying correctness, and deadlock freedom, of such programs is beyond the capabilities of current techniques. For this purpose, we make use of counting predicates that mix counters referring to the number of processes satisfying certain properties and variables directly manipulated by the concurrent processes. We then combine existing works on counter, predicate, and constrained monotonic abstraction and build a nested counter example based refinement scheme for establishing correctness (expressed as non-reachability of configurations satisfying counting predicates formulas). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification on several programs whose correctness crucially depends on precisely capturing the number of processes synchronizing using shared variables.

We introduce Lazy Constrained Monotonic Abstraction (lazy CMA for short) for lazily and soundly exploring well structured abstractions of infinite state non-monotonic systems. CMA makes use of infinite state and well structured abstractions by forcing monotonicity wrt. refinable orderings. The new orderings can be refined based on obtained false positives in a CEGAR like fashion. This allows for the verification of systems that are not monotonic and are hence inherently beyond the reach of classical analysis based on the theory of well structured systems. In this paper, we consistently improve on the existing approach by localizing refinements and by avoiding to trash the explored state space each time a refinement step is required for the ordering. To this end, we adapt ideas from classical lazy predicate abstraction and explain how we address the fact that the number of control points (i.e., minimal elements to be visited) is a priori unbounded. This is unlike the case of plain lazy abstraction which relies on the fact that the number of control locations is finite. We propose several heuristics and report on our experiments using our open source prototype. We consider both backward and forward explorations on non-monotonic systems automatically derived from concurrent programs. Intuitively, the approach could be regarded as using refinable upward closure operators as localized widening operators for an a priori arbitrary number of control points.