skip to main content


Title: Exploiting Simultaneous Multithreading in Priority-Driven Hard Real-Time Systems
Simultaneous Multithreading (SMT) has the ability to dramatically improve real-time scheduling, but existing methods are cumbersome, frequently need specialized hardware, or are limited to producing table-based schedules. Here, an easily portable method for quickly applying SMT to priority-driven hard real-time systems is given. Using a combination of integer linear programming and heuristic bin-packing, a partitioned Earliest-Deadline-First (EDF) scheduler that takes advantage of SMT is produced. The integer linear programming and partitioning are done offline, but generally require only a few seconds, even given over a hundred tasks. A large-scale schedulability study is conducted, showing that compared to partitioned scheduling without SMT, the schedulable utilization for the considered hardware platform is nearly doubled in the best cases.  more » « less
Award ID(s):
1837337
NSF-PAR ID:
10205874
Author(s) / Creator(s):
; ; ;
Date Published:
Journal Name:
Proceedings of the 26th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications
Page Range / eLocation ID:
1 to 10
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. The design of cyber-physical systems (CPSs) requires methods and tools that can efficiently reason about the interaction between discrete models, e.g., representing the behaviors of ``cyber'' components, and continuous models of physical processes. Boolean methods such as satisfiability (SAT) solving are successful in tackling large combinatorial search problems for the design and verification of hardware and software components. On the other hand, problems in control, communications, signal processing, and machine learning often rely on convex programming as a powerful solution engine. However, despite their strengths, neither approach would work in isolation for CPSs. In this paper, we present a new satisfiability modulo convex programming (SMC) framework that integrates SAT solving and convex optimization to efficiently reason about Boolean and convex constraints at the same time. We exploit the properties of a class of logic formulas over Boolean and nonlinear real predicates, termed monotone satisfiability modulo convex formulas, whose satisfiability can be checked via a finite number of convex programs. Following the lazy satisfiability modulo theory (SMT) paradigm, we develop a new decision procedure for monotone SMC formulas, which coordinates SAT solving and convex programming to provide a satisfying assignment or determine that the formula is unsatisfiable. A key step in our coordination scheme is the efficient generation of succinct infeasibility proofs for inconsistent constraints that can support conflict-driven learning and accelerate the search. We demonstrate our approach on different CPS design problems, including spacecraft docking mission control, robotic motion planning, and secure state estimation. We show that SMC can handle more complex problem instances than state-of-the-art alternative techniques based on SMT solving and mixed integer convex programming. 
    more » « less
  2. Existing design techniques for providing security guarantees against network-based attacks in cyber-physical systems (CPS) are based on continuous use of standard cryptographic tools to ensure data integrity. This creates an apparent conflict with common resource limitations in these systems, given that, for instance, lengthy message authentication codes (MAC) introduce significant overheads. We present a framework to ensure both timing guarantees for real-time network messages and Quality-of-Control (QoC) in the presence of network-based attacks. We exploit physical properties of controlled systems to relax constant integrity enforcement requirements, and show how the problem of feasibility testing of intermittently authenticated real-time messages can be cast as a mixed integer linear programming problem. Besides scheduling a set of real-time messages with predefined authentication rates obtained from QoC requirements, we show how to optimally increase the overall system QoC while ensuring that all real-time messages are schedulable. Finally, we introduce an efficient runtime bandwidth allocation method, based on opportunistic scheduling, in order to improve QoC. We evaluate our framework on a standard benchmark designed for CAN bus, and show how an infeasible message set with strong security guarantees can be scheduled if dynamics of controlled systems are taken into account along with real-time requirements. 
    more » « less
  3. Packet scheduling determines the ordering of packets in a queuing data structure with respect to some ranking function that is mandated by a scheduling policy. It is the core component in many recent innovations to optimize network performance and utilization. Our focus in this paper is on the design and deployment of packet scheduling in soft-ware. Software schedulers have several advantages over hardware including shorter development cycle and flexibility in functionality and deployment location. We substantially improve current software packet scheduling performance,while maintaining flexibility, by exploiting underlying features of packet ranking; namely, packet ranks are integers and, at any point in time, fall within a limited range of values.We introduce Eiffel, a novel programmable packet scheduling system. At the core of Eiffel is an integer priority queue based on the Find First Set (FFS) instruction and designed to support a wide range of policies and ranking functions efficiently. As an even more efficient alternative, we also pro-pose a new approximate priority queue that can outperform FFS-based queues for some scenarios. To support flexibility,Eiffel introduces novel programming abstractions to express scheduling policies that cannot be captured by current, state-of-the-art scheduler programming models. We evaluate Eiffel in a variety of settings and in both kernel and userspace deployments. We show that it outperforms state of the art systems by 3-40x in terms of either number of cores utilized for network processing or number of flows given fixed processing capacity 
    more » « less
  4. null (Ed.)
    Iterative computing, where the output accuracy gradually improves over multiple iterations, enables dynamic reconfiguration of energy-quality trade-offs by adjusting the latency (i.e., number of iterations). In order to take full advantage of the dynamic reconfigurability of iterative computing hardware, an efficient method for determining the optimal latency is crucial. In this paper, we introduce an integer linear programming (ILP)-based scheduling method to determine the optimal latency of iterative computing hardware. We consider the input-dependence of output accuracy of approximate hardware using data-driven error modeling for accurate quality estimation. The proposed method finds optimal or near-optimal latency with a significant speedup compared to exhaustive search and decision tree-based optimization. 
    more » « less
  5. Abstract

    Electromagnetic follow-up of gravitational-wave detections is very resource intensive, taking up hours of limited observation time on dozens of telescopes. Creating more efficient schedules for follow-up will lead to a commensurate increase in counterpart location efficiency without using more telescope time. Widely used in operations research and telescope scheduling, mixed-integer linear programming is a strong candidate to produce these higher-efficiency schedules, as it can make use of powerful commercial solvers that find globally optimal solutions to provided problems. We detail a new target-of-opportunity scheduling algorithm designed with Zwicky Transient Facility in mind that uses mixed-integer linear programming. We compare its performance togwemopt, the tuned heuristic scheduler used by the Zwicky Transient Facility and other facilities during the third LIGO–Virgo gravitational-wave observing run. This new algorithm uses variable-length observing blocks to enforce cadence requirements and to ensure field observability, along with having a secondary optimization step to minimize slew time. We show that by employing a hybrid method utilizing both this scheduler andgwemopt, the previous scheduler used, in concert, we can achieve an average improvement in detection efficiency of 3%–11% overgwemoptalone for a simulated binary neutron star merger data set consistent with LIGO–Virgo’s third observing run, highlighting the potential of mixed-integer target of opportunity schedulers for future multimessenger follow-up surveys.

     
    more » « less