Energy intermittency in solar-powered embedded systems threatens Quality of Service (QoS) and system autonomy. In this study, we address the design of these systems with a formal co-design approach that provides verifiable guarantees, a critical advantage over traditional heuristic or predictive methods that often fail under unpredictable conditions. We use timed automata-based modeling within Uppaal Stratego to minimize grid reliance and battery capacity in a typical system, under QoS guarantees. Our methodology demonstrates that synthesized control strategies can reduce grid reliance by 58-72%, while an optimized task scheduling heuristic can decrease required battery capacity by up to 13% compared to the baseline. Our approach provides a formal basis for comparing these techniques to inform system design.

Integrating renewable energy into data centers is essential for reducing reliance on fossil fuels and minimize the environmental impact of digital infrastructures. However, the variability and unpredictability of renewable sources come with significant design and operational challenges. This paper introduces a formal modeling framework for solar-powered small-scale data centers, using stochastic timed automata and statistical model checking for mathematical analysis. The solution supports efficient resource sizing, reduces grid energy consumption through optimized workload scheduling and server renewal strategies. It enables robustness evaluation under component failure scenarios. A case study demonstrates the applicability, flexibility, and scalability of the framework for distributed system topologies and energy-aware design exploration.

This paper defines a data-driven methodology seamlessly combining machine learning (ML) and eXplainable Artificial Intelligence (XAI) techniques to address the challenge of understanding the intricate relationships between microarchitecture mechanisms with respect to system performance. By applying the SHapley Additive exPlanations (SHAP) XAI method, it analyzes the synergies of cache replacement, branch prediction, and hardware prefetching on instructions per cycle (IPC) scores. We validate our methodology by using the SPEC CPU 2006 and 2017 benchmark suites with the ChampSim simulator. We illustrate the benefits of the proposed methodology and discuss the major insights and limitations obtained from this study.

Due to large-scale applications and services, cloud computing infrastructures are experiencing an ever-increasing demand for computing resources. At the same time, the overall power consumption of data centers has been rising beyond 1% of worldwide electricity consumption. The usage of renewable energy in data centers contributes to decreasing their carbon footprint and overall electricity costs. Several green-energy-aware resource allocation approaches have been studied recently. None of them takes advantage of the joint migration ofjobsandenergyin green data centers to increase energy efficiency. This paper presents an optimization approach for energy-efficient resource allocation in mini data centers. The observed momentum around edge computing makes the design of geographically distributed mini data centers highly desirable. Our solution exploits both virtual machines (VMs) and energy migrations between green compute nodes in mini data centers. These nodes have energy harvesting, storage, and transport capabilities. They enable the migration of VMs and energy across different nodes. Compared to VM allocation alone, joint-optimization of VM and energy allocation reduces utility electricity consumption by up to 22%. This reduction can reach up to 28.5% for the same system when integrating less energy-efficient servers. The gains are demonstrated using simulation and a Mixed Integer Linear Programming formulation for the resource allocation problem. Furthermore, we show how our solution contributes to sustaining the energy consumption of old-generation and less efficient servers in mini data centers.

Often suffering from under-optimization, Networks-on-Chip (NoCs) heavily impact the efficiency of domain-specific Systems-on-Chip. To cope with this issue, heterogeneous NoCs are promising alternatives. Nevertheless, the design of optimized NoCs satisfying multiple performance objectives is extremely challenging and requires significant expertise. Prior works failed to combine many objectives or required an extended design space exploration time. In this paper, we propose an approach based on generative artificial intelligence to help pruning complex design spaces for heterogeneous NoCs, according to configurable performance objectives. This is made possible by the ability of Generative Adversarial Networks to learn and generate relevant design candidates for the target NoCs. The speed and flexibility of our solution enable a fast generation of optimized NoCs that fit users' expectations. Through some experiments, we show how to obtain competitive NoC designs reducing the power consumption with no communication performance or area penalty compared to a given conventional NoC design.

A Network-on-Chip (NoC) is an essential component of a chip multiprocessor (CMP) which however contributes to a large fraction of system energy. The unpredictability of traffic across a NoC frequently involves an expensive over-sizing of NoC resources which in turn leads to a significant contribution to the CMP power consumption. There exists a body of work addressing this issue, however so far solutions fall short when aiming for power reduction whilst maintaining high NoC performance. This paper proposes to combine router architecture optimizations with smart resource management to overcome this limitation. Based on a fully segmented architecture, we present an online adaptive router adjusting its active routing resources to meet the current traffic demand. This enhanced power-gating strategy significantly decreases both static and dynamic power consumption of the NoC, up to 70% for synthetic traffic patterns and up to 58% for real traffic workloads, while preserving NoC latency and throughput. Thanks to these adaptive power-saving mechanisms the proposed segmented NoC router provides near energy-proportional operation across the range of used benchmarks.

Energy-driven computing is a recent paradigm that promotes energy harvesting as an alternative solution to conventional power supply systems. A crucial challenge in that context lies in the dimensioning of system resources w.r.t. energy harvesting conditions while meeting some given timing QoS requirements. Existing simulation and debugging tools do not make it possible to clearly address this issue. This paper defines a generic modeling and analysis framework to support the design exploration for energy-driven computing. It uses stochastic hybrid automata and statistical model-checking. It advocates a distributed system design, where heterogeneous nodes integrate computing and harvesting components and support inter-node energy transfer. Through a simple case-study, the paper shows how this framework addresses the aforementioned design challenge in a flexible manner and helps in reducing energy storage requirements.

A hardware configuration is a set of processors and their frequency levels in a multicore heterogeneous system. This article presents a compiler-based technique to match functions with hardware configurations. Such a technique consists of using multivariate linear regression to associate function arguments with particular hardware configurations. By showing that this classification space tends to be convex in practice, this article demonstrates that linear regression is not only an efficient tool to map computations to heterogeneous hardware, but also an effective one. To demonstrate the viability of multivariate linear regression as a way to perform adaptive compilation for heterogeneous architectures, we have implemented our ideas onto the Soot Java bytecode analyzer. Code that we produce can predict the best configuration for a large class of Java and Scala benchmarks running on an Odroid XU4 big.LITTLE board; hence, outperforming prior techniques such as ARM’s GTS and CHOAMP, a recently released static program scheduler.

Energy-aware architectures provide applications with a mix of low and high frequency cores. Selecting the best core configurations for running programs is very challenging. Here, we leverage compilation, runtime monitoring and machine learning to map program phases to their best matching configurations. As a proof-of-concept, we devise the Astro system to show that our approach can outperform a state-of-the-art Linux scheduler for heterogeneous architectures.

A store operation is called “silent” if it writes in memory a value that is already there. The ability to detect silent stores is important, because they might indicate performance bugs, might enable code optimizations, and might reveal opportunities of automatic parallelization, for instance. Silent stores are traditionally detected via profiling tools. In this article, we depart from this methodology and instead explore the following question: is it possible to predict silentness by analyzing the syntax of programs? The process of building an answer to this question is interesting in itself, given the stochastic nature of silent stores, which depend on data and coding style. To build such an answer, we have developed a methodology to classify store operations in terms of syntactic features of programs. Based on such features, we develop different kinds of predictors, some of which go much beyond what any trivial approach could achieve. To illustrate how static prediction can be employed in practice, we use it to optimize programs running on nonvolatile memory systems.

As we close out the year 2018, it is time to reflect back a number of milestones achieved throughout the year. The transition to the new EIC and team included a 50-member editorial board with 19 new members selected after an extensive round of open call for editorial board nominations. While, this was a reduction in the editorial board from 66 members previously, the response time remained steady at about two months from submission to first decision. As of this writing in December, we received 469 new manuscripts as well as 371 revised manuscripts in 2018. The top two departments with substantial lead over the rest were “Modeling and Simulation” and “Emerging Technologies and Applications.”

Current main memory organizations in embedded and mobile application systems are DRAM dominated. The ever-increasing gap between today's processor and memory speeds makes the DRAM subsystem design a major aspect of computer system design. However, the limitations to DRAM scaling and other challenges like refresh provide undesired trade-offs between performance, energy and area to be made by architecture designers. Several emerging NVM options are being explored to at least partly remedy this but today it is very hard to assess the viability of these proposals because the simulations are not fully based on realistic assumptions on the NVM memory technologies and on the system architecture level. In this paper, we propose to use realistic, calibrated STT-MRAM models and a well calibrated cross-layer simulation and exploration framework, named SEAT, to better consider technologies aspects and architecture constraints. We will focus on general purpose/mobile SoC multi-core architectures. We will highlight results for a number of relevant benchmarks, representatives of numerous applications based on actual system architecture. The most energy efficient STT-MRAM based main memory proposal provides an average energy consumption reduction of 27% at the cost of 2x the area and the least energy efficient STT-MRAM based main memory proposal provides an average energy consumption reduction of 8% at the around the same area or lesser when compared to DRAM.

For monolithic heterogeneous integration, fast yet low-power processing and storage, and high integration density, the objective of the EU GREAT project is to co-integrate multiple digital and analog functions together within CMOS by adapting the Magnetic Tunneling Junctions (MTJs) into a single baseline technology enabling logic, memory, and analog functions, particularly for Internet of Things (IoT) platforms. This will lead to a unique STT-MTJ cell technology called Multifunctional Standardized Stack (MSS). This paper presents the progress in the project from the technology, compact modeling, process design kit, standard cells, as well as memory and system level design evaluation and exploration. The proposed technology and toolsets are giant leaps towards heterogeneous integrated technology and architectures for IoT.

The scaling limits of CMOS have pushed many researchers to explore alternative technologies for beyond CMOS circuits. In addition to the increased device variability and process complexity led by the continuous decreasing size of CMOS transistors, heat dissipation effects limit the density and speed of current systems-on-chip. For beyond CMOS systems, the emerging memory technology STT-MRAM is seen as a promising alternative solution. This paper shows first how STT-MRAM can improve energy efficiency and reliability of future embedded systems. Then, a hybrid design exploration framework is presented to investigate the potential of STT-MRAM for high performance computing.

Network-on-Chip provides scalable communication in Systems-on-Chip with many Intellectual Property cores. Studies have shown that unutilized router buffers lead to significant network performance degradation. This work presents Roundabout, a new asynchronous router architecture with inherent and effective buffer utilization. Inspired by real-life multi-lane roundabouts, it consists of lanes shared by input and output ports. A prototype of Roundabout is evaluated using 45nm CMOS technology. The router is able to achieve a throughput of 465 Mflit/sec. It achieves a network saturation threshold of 129 Gbps on a 4x4 Mesh topology network. Roundabout performance, area and power results are competitive with existing synchronous and asynchronous solutions. It provides good topological tradeoffs for significantly improving network performance without corresponding area overhead.

Most Network-on-Chip routers dedicate a set of buffers to the input and/or output ports. This design decision leads to buffer underutilization especially when running applications with non-uniform traffic patterns. In order to maximize resource usage for performance and energy gains, we present a synchronous and elastic buffer implementation of a router architecture called Roundabout with intrinsic resource sharing. Roundabout is inspired by real-life traffic roundabouts and consists of lanes shared by multiple input and output ports. Roundabout offers performance improvement of 61% for uniform traffic pattern and up to 88% for non-uniform traffic pattern over the Hermes router, a typical input buffered router. In terms of power, it consumes 24% less than the Hermes router. Roundabout provides a highly parametric architecture that can produce different router configurations with varying topological trade-offs for performance gains without sacrificing area.

Over the past few years, a new era of smart connected devices has emerged in the market to enable the future world of the Internet of Things (IoT). A key requirement for IoT applications is the power consumption to allow very high autonomy in the case of battery-powered systems. Depending on the application, such devices will be most of the time in a low-power mode (sleep mode) and will wake up only when there is a task to accomplish (active mode). Emerging non-volatile memory technologies are seen as a very attractive solution to design ultra-low-power systems. Among these technologies, magnetic random access memory is a promising candidate, as it combines non-volatility, high density, reasonable latency, and low leakage. Integration of non-volatility as a new feature of memories has the great potential to allow full data retention after a complete shutdown with a fast wake-up time. This article explores the benefits of having a non-volatile processor to enable ultra-low-power IoT devices.

A large portion of existing multithreaded embedded software has been programmed according to symmetric shared memory platforms where a monolithic memory block is shared by all cores. Such platforms accommodate popular parallel programming models such as POSIX threads and OpenMP. However with the growing number of cores in modern manycore embedded architectures, they present a bottleneck related to their centralized memory accesses. This paper proposes a solution tailored for an efficient execution of applications defined with shared-memory programming models onto on-chip distributed-memory multicore architectures. It shows how performance, area and energy consumption are significantly improved thanks to the scalability of these architectures. This is illustrated in an open-source realistic design framework, including tools from ASIC to microkernel.

Dynamically reconfigurable hardware has been identified as a promising solution for the design of energy-efficient embedded systems. However, its adoption is limited by costly design effort, including verification and validation, which is even more complex than for nondynamically reconfigurable systems. In this article, we propose a tool-supported formal method to automatically design a correct-by-construction control of the reconfiguration. By representing system behaviors with automata, we exploit automated algorithms to synthesize controllers that safely enforce reconfiguration strategies formulated as properties to be satisfied by control. We design generic modeling patterns for a class of reconfigurable architectures, taking into account both hardware architecture and applications, as well as relevant control objectives. We validate our approach on two case studies implemented on FPGAs.

International audience

This paper presents a cost-effective and formal approach to model and analyze streaming applications on multi-processor systems-on-chip (MPSoCs). This approach enables to address time requirements, mapping of applications on MPSoCs and system behavior correctness by using abstract clocks of synchronous languages. Compared to usual prototyping and simulation techniques, it is very fast and favors correctness-by-construction. No coding is needed to run and analyze a system, which avoids tedious debugging efforts. It is an ideal complement to existing techniques to deal with large system design spaces.

In this paper, we present a method for the design of MPSoCs for complex data-intensive applications. This method aims at a blend exploration of the communication, the memory system architecture and the computation resource parallelism. The proposed method is exemplified on a JPEG Encoder case study by describing all the design steps. Our method allows for a JPEG encoder implementation having a throughput increase of 84% and an increase of the achievable FPGA maximum frequency fmaxof 64% with an area overhead of 6 with respect to a reference solution. Our method is also assessed with additional explorations of applications from different domains.

This paper presents an approach advocating abstract clocks to represent data-intensive applications executed on multiprocessor systems-on-chip (MPSoCs) for facilitating the exploration of large design spaces. By using abstract clocks, the advocated method characterizes applications defined by multiple loop nests, as well as, useful loop transformations that contribute to an efficient application execution. It combines the advantages of optimizations provided by loop transformations and the precision of information on scheduling captured by the abstract clocks. As a result, it favors a rapid, and yet accurate design space exploration (DSE) of data-intensive systems.

International audience

Polychronous specifications express concurrent, multi-clocked models which capture multiple threads of computation operating relatively asynchronous to each other. A clock of a variable in this context, is the totally ordered set of instants at which events occur on that variables. However, the notion of instant here is logical as opposed to real-time instants. The instants of different clocks may be partially ordered. The executable code synthesis from Polychronous specifications relies on computation of schedules through clock calculus. Unfortunately, it is often hard to distinguish from true causal loops which cause deadlocks from apparent causal loops which do not. The SIGNAL compiler in the Polychrony tool-set currently rejects all programs with apparent causal loops, thus rejecting a large set of valid specifications. A recently developed polychronous formalism MRICDF and its tool-set EmCodeSyn do the same. Even in the Polychrony literature, the deadlock causing loop detection based on Boolean satisfiability is not enough to discern all possible false loops, thereby still rejecting a lot of valid specifications. In order to not reject programs whose apparent loops are never realizable, a theory of reals or integers or other data types are required. In this paper, we formulate the detection of false loops in MRICDF as a decision problem in Satisfiability Modulo Theory (SMT). Due to recent interests in SMT solvers, a number of efficient solvers are available which offer a greater expressiveness in dealing with non Boolean constraints and allow us to discern false loops from realizable causalities in reasonable computation time. This paper proposes an SMT based synthesis technique which demonstrates that several polychronous specifications rejected by the Polychrony/EmCodeSyn synthesis tools due to their inability to identify only true causal loops, can be synthesized as correct sequential embedded software.

Modern embedded systems integrate more and more complex functionalities. At the same time, the semiconductor technology advances enable to increase the amount of hardware resources on a chip for the execution. Massively parallel embedded systems specifically deal with the optimized usage of such hardware resources to efficiently execute their functionalities. The design of these systems mainly relies on the following challenging issues: first, how to deal with the parallelism in order to increase the performance; second, how to abstract their implementation details in order to manage their complexity; third, how to refine these abstract representations in order to produce efficient implementations. This article presents the Gaspard design framework for massively parallel embedded systems as a solution to the preceding issues. Gaspard uses the repetitive Model of Computation (MoC), which offers a powerful expression of the regular parallelism available in both system functionality and architecture. Embedded systems are designed at a high abstraction level with the MARTE (Modeling and Analysis of Real-time and Embedded systems) standard profile, in which our repetitive MoC is described by the so-called Repetitive Structure Modeling (RSM) package. Based on the Model-Driven Engineering (MDE) paradigm, MARTE models are refined towards lower abstraction levels, which make possible the design space exploration. By combining all these capabilities, Gaspard allows the designers to automatically generate code for formal verification, simulation and hardware synthesis from high-level specifications of high-performance embedded systems. Its effectiveness is demonstrated with the design of an embedded system for a multimedia application.

This paper presents an operational semantics of the repetitive model of computation, which is the basis for the repetitive structure modeling (RSM) package defined in the standard UML Marte profile. It also deals with the semantics of an RSM extension for control-oriented design. The goal of this semantics is to serve as a formal support for i) reasoning about the behavioral properties of models specified in Marte with RSM, and ii) defining correct-by-construction model transformations for the production of executable code in a model-driven engineering framework.

This paper presents the design of distributed embedded systems using the synchronous multiclock model of the SIGNAL language. It proposes a methodology that ensures a correct-by-construction functional implementation of these systems from high-level models. It shows the capability of the synchronous approach to apply formal techniques and tools that guarantee the reliability of the designed systems. Such a capability is necessary and highly worthy when dealing with safety-critical systems. The proposed methodology is demonstrated through a case study consisting of a simple avionic application, which aims to pragmatically help the reader to understand the manipulated formal concepts, and to apply them easily in order to solve system correctness issues encountered in practice. The application functionality is first modeled as well as its distribution on a generic hardware architecture. This relies on the endochrony and endo-isochrony properties of SIGNAL specifications, defined previously. The considered architectures include asynchronous communication mechanisms, which are also modeled in SIGNAL and proved to achieve message exchanges correctly. Furthermore, the synchronizability of the different parts in the resulting system is addressed after its deployment on a specific execution platform with multirate clocks. After all these steps, a distributed code can be automatically generated.

This paper addresses the design issue of System-on-Chip by elevating the design abstraction levels, through a model-driven approach. It considers the standard Marte profile, which is dedicated to the Modeling and Analysis of Real-Time Embedded systems. From user-defined models, information are extracted, which serve for the analysis of the models. The adopted analysis technique relies on the synchronous reactive approach, which strongly favors formal validation.

Digital television (DTV) is an advanced broadcasting technology that is spreading fast today. It gives broadcasters the capability to send programs with a better picture and sound quality. Moreover, broadcasters can send several programming choices, called multicasting. DTV consists of a high-performance system combining both control and intensive data processing. In this paper, we first show how the OMG MARTE profile can serve to model such a system. Then, we use the synchronous approach to formally check some temporal properties of the expected system implementation for validation purpose.

This paper presents an approach for the modeling and formalvalidation of high-performance systems. The approach relies on the repetitive model of computation used to express the parallelism of such systems within the Gaspard framework, which is dedicated to the codesign of high-performance system-on-chip. The system descriptions obtained with this model are then projected on the synchronous model of computation. The result of this projectionconsists of an equational model that allows one to formally analyze clock synchronizability issues so as to guarantee the reliable deployment of systems on platforms.

Embedded real-time systems consist of hardware and software that controls the behavior of a device or plant. They are ubiquitous in today's technological landscape and found in domains such as telecommunications, nuclear power, avionics, and medical technology. These systems are difficult to design and build because they must satisfy both functional and timing requirements to work correctly in their intended environment. Furthermore, embedded systems are often critical systems, where failure can lead to loss of life, loss of mission, or serious financial consequences. Because of the difficulty in creating these systems and the consequences of failure, they require rigorous and reliable design approaches. The synchronous approach is one possible answer to this demand. Its mathematical basis provides formal concepts that favor the trusted design of embedded real-time systems. The multiclock or polychronous model stands out from other synchronous specification models by its capability to enable the design of systems where each component holds its own activation clock as well as single-clocked systems in a uniform way. A great advantage is its convenience for component-based design approaches that enable modular development of increasingly complex modern systems. The expressiveness of its underlying semantics allows dealing with several issues of real-time design. This article exposes insights gained during recent years from the design of real-time applications within the polychronous framework. In particular, it shows promising results about the design of applications from the avionics domain.

Among related synchronous programming principles, the model of computation of the POLYCHRONY workbench stands out by its capability to give high-level description of systems where each component owns a local activation clock (such as, typically,distributed real-time systems or systems on a chip). In order to bring the modeling capability of POLYCHRONY to the context of a model-driven engineering toolset for embedded system design, we define a diagramic notation composed of mode automata and data-flow equations on top of the multi-clocked synchronous model of computation supported by the POLYCHRONY workbench. We demonstrate the agility of this paradigm by considering the example of an integrated modular avionics application. Our presentation features the formalization and use of model transformation techniques of the GME environment to embed the extension of POLYCHRONY's meta-model with mode automata.