| 1. |
- Horga, Adrian, 1989-
(author)
-
Performance and Security Analysis for GPU-Based Applications
- 2022
-
Doctoral thesis (other academic/artistic)abstract
- Graphics Processing Units (GPUs) are becoming more and more prevalent in general-purpose computing. GPUs are used in areas from embedded systems to super-computing. With applications ranging from fluid dynamics simulations to image processing, machine learning, and encryption, GPU programs need to satisfy not only performance requirements but also various other non-functional constraints. Besides the aspects regarding performance, also security and the worst case execution time (WCET) need to be considered for such GPU applications. In our work, we study such non-functional properties and present approaches to detect and solve issues regarding them.First, we focus on the performance of GPU applications by detecting cache related performance bottlenecks. We detect the root causes of such bottlenecks and provide solutions to reduce their negative impact on performance. We also discuss and compare the impact of cache replacement policies and thread scheduling policies on the performance of GPU applications.Then, we present a measurement-based technique, which combines symbolic execution and genetic algorithms, and is used for estimating the WCET of GPU programs. Our proposed technique helps to produce test inputs that lead towards the WCET of a program. We also propose solutions to alleviate the inherent complexity of GPU programs due to branching behavior and high number of threads running in parallel.In continuation, we propose a technique to expose the side-channel leakage of shared memory in GPU implementations of cryptographic algorithms. We evaluate the robustness of such algorithms in the context of shared memory side-channel leakage. Also, we discuss the security and side-channel leakage for different implementations of the same algorithm.Finally, a formal approach is presented for the detection of GPU shared memory bank conflicts. We explore and discuss the impact of such conflicts on the performance and security of GPU applications. We show how our approach can help in producing inputs that can lead towards the WCET. We also discuss how our approach can be used to evaluate the leakage of the shared memory side-channel for GPU implementations of cryptographic algorithms.
|
|
| 2. |
- Ganjei, Zeinab, 1989-
(author)
-
Parameterized Verification of Synchronized Concurrent Programs
- 2021
-
Doctoral thesis (other academic/artistic)abstract
- There is currently an increasing demand for concurrent programs. Checking the correctness of concurrent programs is a complex task due to the interleavings of processes. Sometimes, violation of the correctness properties in such systems causes human or resource losses; therefore, it is crucial to check the correctness of such systems. Two main approaches to software analysis are testing and formal verification. Testing can help discover many bugs at a low cost. However, it cannot prove the correctness of a program. Formal verification, on the other hand, is the approach for proving program correctness. Model checking is a formal verification technique that is suitable for concurrent programs. It aims to automatically establish the correctness (expressed in terms of temporal properties) of a program through an exhaustive search of the behavior of the system. Model checking was initially introduced for the purpose of verifying finite‐state concurrent programs, and extending it to infinite‐state systems is an active research area.In this thesis, we focus on the formal verification of parameterized systems. That is, systems in which the number of executing processes is not bounded a priori. We provide fully-automatic and parameterized model checking techniques for establishing the correctness of safety properties for certain classes of concurrent programs. We provide an open‐source prototype for every technique and present our experimental results on several benchmarks.First, we address the problem of automatically checking safety properties for bounded as well as parameterized phaser programs. Phaser programs are concurrent programs that make use of the complex synchronization construct of Habanero Java phasers. For the bounded case, we establish the decidability of checking the violation of program assertions and the undecidability of checking deadlock‐freedom. For the parameterized case, we study different formulations of the verification problem and propose an exact procedure that is guaranteed to terminate for some reachability problems even in the presence of unbounded phases and arbitrarily many spawned processes. Second, we propose an approach for automatic verification of parameterized concurrent programs in which shared variables are manipulated by atomic transitions to count and synchronize the spawned processes. For this purpose, we introduce counting predicates that related counters that refer to the number of processes satisfying some given properties to the variables that are directly manipulated by the concurrent processes. We then combine existing works on the counter, predicate, and constrained monotonic abstraction and build a nested counterexample‐based refinement scheme to establish correctness. Third, we introduce Lazy Constrained Monotonic Abstraction for more efficient exploration of well‐structured abstractions of infinite‐state non‐monotonic systems. We propose several heuristics and assess the efficiency of the proposed technique by extensive experiments using our open‐source prototype. Lastly, we propose a sound but (in general) incomplete procedure for automatic verification of safety properties for a class of fault‐tolerant distributed protocols described in the Heard‐Of (HO for short) model. The HO model is a popular model for describing distributed protocols. We propose a verification procedure that is guaranteed to terminate even for unbounded number of the processes that execute the distributed protocol.
|
|
| 3. |
- Zhou, Yuanbin, 1991-
(author)
-
Synthesis of Safety-Critical Real-Time Systems
- 2022
-
Doctoral thesis (other academic/artistic)abstract
- Modern safety-critical real-time systems are becoming more and more complex, due to sophisticated applications such as advanced driving assistance, automated driving, advanced infotainment, and applications involving machine learning and deep learning. This has led to increased requirements for the communication infrastructures. Real-time bus-based communication techniques, such as CAN and FlexRay, have been widely adopted for decades, due to their low cost and reliable communication capability. However, the bandwidth provided by these technologies is often not enough for modern safety-critical systems. Time-Sensitive Networking (TSN) is a promising technique that can handle the increasing bandwidth requirements, while meeting real-time constraints and providing Ethernet compatible solutions. We have studied the synthesis of schedules and routes for TSN, in order to fulfill timing and reliability requirements for safety-critical systems. Functional safety is an important goal for such systems, to ensure that no unreasonable risks are taken. This involves handling random and systematic faults, both of which are considered in this work. We synthesize schedules and routes for TSN so that the probability of faulty transmission due to random faults is below a certain threshold.ASIL Decomposition, introduced in the automotive industry, is applied to handle systematic faults, while achieving overall cost minimization. In order to improve schedulability, preemption support in TSN has also been studied. Heuristic algorithms are proposed for all the above contributions to address scalability issues characterized for the constrained synthesis and optimization problem addressed.Traditional designs for safety-critical systems usually deploy a federated architecture, where several processors are available and each processor implements one dedicated function. An important goal is to achieve fault containment. However, due to the increasing complexity of modern safety-critical systems, this architecture is no longer scalable. Therefore, several tasks with different criticality levels are usually integrated on the same computing platform. A key aspect for such systems is to achieve the required independence between tasks at different criticality levels and to guarantee that they do not interfere each other. We have developed a partitioned scheduling technique for mixed-criticality systems to achieve temporal independence, while minimizing the CPU usage.
|
|
| 4. |
- Maghazeh, Arian, 1985-
(author)
-
System-Level Design of GPU-Based Embedded Systems
- 2018
-
Doctoral thesis (other academic/artistic)abstract
- Modern embedded systems deploy several hardware accelerators, in a heterogeneous manner, to deliver high-performance computing. Among such devices, graphics processing units (GPUs) have earned a prominent position by virtue of their immense computing power. However, a system design that relies on sheer throughput of GPUs is often incapable of satisfying the strict power- and time-related constraints faced by the embedded systems.This thesis presents several system-level software techniques to optimize the design of GPU-based embedded systems under various graphics and non-graphics applications. As compared to the conventional application-level optimizations, the system-wide view of our proposed techniques brings about several advantages: First, it allows for fully incorporating the limitations and requirements of the various system parts in the design process. Second, it can unveil optimization opportunities through exposing the information flow between the processing components. Third, the techniques are generally applicable to a wide range of applications with similar characteristics. In addition, multiple system-level techniques can be combined together or with application-level techniques to further improve the performance.We begin by studying some of the unique attributes of GPU-based embedded systems and discussing several factors that distinguish the design of these systems from that of the conventional high-end GPU-based systems. We then proceed to develop two techniques that address an important challenge in the design of GPU-based embedded systems from different perspectives. The challenge arises from the fact that GPUs require a large amount of workload to be present at runtime in order to deliver a high throughput. However, for some embedded applications, collecting large batches of input data requires an unacceptable waiting time, prompting a trade-off between throughput and latency. We also develop an optimization technique for GPU-based applications to address the memory bottleneck issue by utilizing the GPU L2 cache to shorten data access time. Moreover, in the area of graphics applications, and in particular with a focus on mobile games, we propose a power management scheme to reduce the GPU power consumption by dynamically adjusting the display resolution, while considering the user's visual perception at various resolutions. We also discuss the collective impact of the proposed techniques in tackling the design challenges of emerging complex systems.The proposed techniques are assessed by real-life experimentations on GPU-based hardware platforms, which demonstrate the superior performance of our approaches as compared to the state-of-the-art techniques.
|
|
| 5. |
- Mahfouzi, Rouhollah, 1989-
(author)
-
Security-Aware Design of Cyber-Physical Systems for Control Applications
- 2021
-
Doctoral thesis (other academic/artistic)abstract
- With cyber-physical systems opening to the outside world, security can no longer be considered a secondary issue. In this work, we focus on security threats to control applications in cyber-physical systems. We provide detection, prevention, and mitigation solutions to attacks considering the stringent resource constraints and important properties of such systems. First, we highlight some important properties of control applications that are used to design an intrusion detection and mitigation mechanism. We show how the control laws, derived from the physical properties of control applications, can facilitate the intrusion detection mechanism. We also use a resource management approach to maintain the performance of the control application under attack. Second, we elaborate on the challenges derived from sharing a processor among several controller tasks. We investigate the counter-intuitive timing anomalies that result from such resource sharing and introduce the Butterfly attack which exploits these anomalies. With the Butterfly attack, the adversary interferes with a low criticality and less protected task to change the timing behavior of the other tasks sharing the same platform. We experimentally show how this attack can indirectly destabilize a high criticality and, potentially, more protected task. Then, we consider real-time communication of control applications over a Time-Triggered Ethernet network. We demonstrate the impact of varying delays on control stability and identify the route and schedule constraints that are necessary to guarantee stability. On top of that, we study the impact of encryption and decryption delays on stability and employ a design space exploration approach to maximize security while continuing to satisfy stability guarantees.
|
|
| 6. |
- Ukhov, Ivan, 1986-
(author)
-
System-Level Analysis and Design under Uncertainty
- 2017
-
Doctoral thesis (other academic/artistic)abstract
- One major problem for the designer of electronic systems is the presence of uncertainty, which is due to phenomena such as process and workload variation. Very often, uncertainty is inherent and inevitable. If ignored, it can lead to degradation of the quality of service in the best case and to severe faults or burnt silicon in the worst case. Thus, it is crucial to analyze uncertainty and to mitigate its damaging consequences by designing electronic systems in such a way that uncertainty is effectively and efficiently taken into account.We begin by considering techniques for deterministic system-level analysis and design of certain aspects of electronic systems. These techniques do not take uncertainty into account, but they serve as a solid foundation for those that do. Our attention revolves primarily around power and temperature, as they are of central importance for attaining robustness and energy efficiency. We develop a novel approach to dynamic steady-state temperature analysis of electronic systems and apply it in the context of reliability optimization.We then proceed to develop techniques that address uncertainty. The first technique is designed to quantify the variability in process parameters, which is induced by process variation, across silicon wafers based on indirect and potentially incomplete and noisy measurements. The second technique is designed to study diverse system-level characteristics with respect to the variability originating from process variation. In particular, it allows for analyzing transient temperature profiles as well as dynamic steady-state temperature profiles of electronic systems. This is illustrated by considering a problem of design-space exploration with probabilistic constraints related to reliability. The third technique that we develop is designed to efficiently tackle the case of sources of uncertainty that are less regular than process variation, such as workload variation. This technique is exemplified by analyzing the effect that workload units with uncertain processing times have on the timing-, power-, and temperature-related characteristics of the system under consideration.We also address the issue of runtime management of electronic systems that are subject to uncertainty. In this context, we perform an early investigation into the utility of advanced prediction techniques for the purpose of fine-grained long-range forecasting of resource usage in large computer systems.All the proposed techniques are assessed by extensive experimental evaluations, which demonstrate the superior performance of our approaches to analysis and design of electronic systems compared to existing techniques.
|
|
