SMT-Based Contention-Free Task Mapping and Scheduling on 2D/3D SMART NoC with Mixed Dimension-Order Routing

SMART NoCs achieve ultra-low latency by enabling single-cycle multiple-hop transmission via bypass channels. However, contention along bypass channels can seriously degrade the performance of SMART NoCs by breaking the bypass paths. Therefore, contention-free task mapping and scheduling are essential for optimal system performance. In this article, we propose an SMT (Satisfiability Modulo Theories)-based framework to find optimal contention-free task mappings with minimum application schedule lengths on 2D/3D SMART NoCs with mixed dimension-order routing. On top of SMT’s fast reasoning capability for conditional constraints, we develop efficient search-space reduction techniques to achieve practical scalability. Experiments demonstrate that our SMT framework achieves 10× higher scalability than ILP (Integer Linear Programming) with 931.1× (ranges from 2.2× to 1532.1×) and 1237.1× (ranges from 4× to 4373.8×) faster average runtimes for finding optimum solutions on 2D and 3D SMART NoCs and our 2D and 3D extensions of the SMT framework with mixed dimension-order routing also maintain the improved scalability with the extended and diversified routing paths, resulting in reduced application schedule lengths throughout various application benchmarks.

Embedding and extraction of knowledge in tree ensemble classifiers

The embedding and extraction of knowledge is a recent trend in machine learning applications, e.g., to supplement training datasets that are small. Whilst, as the increasing use of machine learning models in security-critical applications, the embedding and extraction of malicious knowledge are equivalent to the notorious backdoor attack and defence, respectively. This paper studies the embedding and extraction of knowledge in tree ensemble classifiers, and focuses on knowledge expressible with a generic form of Boolean formulas, e.g., point-wise robustness and backdoor attacks. For the embedding, it is required to be preservative (the original performance of the classifier is preserved), verifiable (the knowledge can be attested), and stealthy (the embedding cannot be easily detected). To facilitate this, we propose two novel, and effective embedding algorithms, one of which is for black-box settings and the other for white-box settings. The embedding can be done in PTIME. Beyond the embedding, we develop an algorithm to extract the embedded knowledge, by reducing the problem to be solvable with an SMT (satisfiability modulo theories) solver. While this novel algorithm can successfully extract knowledge, the reduction leads to an NP computation. Therefore, if applying embedding as backdoor attacks and extraction as defence, our results suggest a complexity gap (P vs. NP) between the attack and defence when working with tree ensemble classifiers. We apply our algorithms to a diverse set of datasets to validate our conclusion extensively.

Constraint Answer Set Programming: Integrational and Translational (or SMT-based) Approaches

Constraint answer set programming or CASP, for short, is a hybrid approach in automated reasoning putting together the advances of distinct research areas such as answer set programming, constraint processing, and satisfiability modulo theories. CASP demonstrates promising results, including the development of a multitude of solvers: acsolver, clingcon, ezcsp, idp, inca, dingo, mingo, aspmt2smt, clingo[l,dl], and ezsmt. It opens new horizons for declarative programming applications such as solving complex train scheduling problems. Systems designed to find solutions to constraint answer set programs can be grouped according to their construction into, what we call, integrational or translational approaches. The focus of this paper is an overview of the key ingredients of the design of constraint answer set solvers drawing distinctions and parallels between integrational and translational approaches. The paper also provides a glimpse at the kind of programs its users develop by utilizing a CASP encoding of Traveling Salesman problem for illustration. In addition, we place the CASP technology on the map among its automated reasoning peers as well as discuss future possibilities for the development of CASP.

Functional verification of cyber-physical systems containing machine-learnt components

Functional architectures of cyber-physical systems increasingly comprise components that are generated by training and machine learning rather than by more traditional engineering approaches, as necessary in safety-critical application domains, poses various unsolved challenges. Commonly used computational structures underlying machine learning, like deep neural networks, still lack scalable automatic verification support. Due to size, non-linearity, and non-convexity, neural network verification is a challenge to state-of-art Mixed Integer linear programming (MILP) solvers and satisfiability modulo theories (SMT) solvers [2], [3]. In this research, we focus on artificial neural network with activation functions beyond the Rectified Linear Unit (ReLU). We are thus leaving the area of piecewise linear function supported by the majority of SMT solvers and specialized solvers for Artificial Neural Networks (ANNs), the successful like Reluplex solver [1]. A major part of this research is using the SMT solver iSAT [4] which aims at solving complex Boolean combinations of linear and non-linear constraint formulas (including transcendental functions), and therefore is suitable to verify the safety properties of a specific kind of neural network known as Multi-Layer Perceptron (MLP) which contain non-linear activation functions.

Politeness for the Theory of Algebraic Datatypes (Extended Abstract)

Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing also how it can be combined with other arbitrary disjoint theories using polite combination. Our results cover both inductive and finite datatypes, as well as their union. The combination method uses a new, simple, and natural notion of additivity, that enables deducing strong politeness from (weak) politeness.

Algorithmic Reduction of Biological Networks with Multiple Time Scales

We present a symbolic algorithmic approach that allows to compute invariant manifolds and corresponding reduced systems for differential equations modeling biological networks which comprise chemical reaction networks for cellular biochemistry, and compartmental models for pharmacology, epidemiology and ecology. Multiple time scales of a given network are obtained by scaling, based on tropical geometry. Our reduction is mathematically justified within a singular perturbation setting. The existence of invariant manifolds is subject to hyperbolicity conditions, for which we propose an algorithmic test based on Hurwitz criteria. We finally obtain a sequence of nested invariant manifolds and respective reduced systems on those manifolds. Our theoretical results are generally accompanied by rigorous algorithmic descriptions suitable for direct implementation based on existing off-the-shelf software systems, specifically symbolic computation libraries and Satisfiability Modulo Theories solvers. We present computational examples taken from the well-known BioModels database using our own prototypical implementations.

Leveraging Control Flow Knowledge in SMT Solving of Program Verification

Satisfiability modulo theories (SMT) solvers have been widely applied as the reasoning engine for diverse software analysis and verification technologies. The efficiency of the SMT solver has significant effects on the performance of these technologies. However, current SMT solvers are designed for the general purpose of constraint solving. Lots of useful knowledge of programs cannot be utilized during SMT solving. As a result, the SMT solver may spend much effort to explore redundant search space. In this article, we propose a novel approach to utilizing control-flow knowledge in SMT solving. With this technique, the search space can be considerably reduced, and the efficiency of SMT solving is observably improved. We conducted extensive experiments on credible benchmarks. The results show significant improvements of our approach.

A conflicts’ classification for IoT-based services: a comparative survey

Recently, Internet of Things (IoT)-based systems, especially automation systems, have become an indispensable part of modern-day lives to support the controlling of the networked devices and providing context-aware and intelligent environments. IoT-based services/apps developed by the end-users interact with each other and share concurrent access to devices according to their preferences, which increases safety, security, and correctness issues in IoT systems. Due to the critical impacts resulting from these issues, IoT-based apps require a customized type of compilers or checking tools that capable of analyzing the structures of these apps and detecting different types of errors and conflicts either in intra-IoT app instructions or in inter-IoT apps interactions. A plethora of approaches and frameworks have been proposed to assist the best practices for end-users in developing their IoT-based apps and mitigate these errors and conflicts. This paper focuses on conflict classification and detection approaches in the context of IoT systems by investigating the current research techniques that provided conflicts’ classification or detection in IoT systems (published between 2014 and 2020). A classification of IoT-based apps interaction conflicts is proposed. The proposed conflicts’ classification provides a priori conflicts detection method based on the analysis of IoT app instructions’ relationships with utilizing the state-of-the-art Satisfiability Modulo Theories (SMT) model checking and formal notations. The current detection approaches are compared with each other according to the proposed conflicts’ classification to determine to which extend they cover different conflicts. Based on this comparison, we provide evidence that the existing approaches have a gap in covering different conflicts’ levels and types which yields to minimize the correctness and safety of IoT systems. We point out the need to develop a safety and security compiler or tool for IoT systems. Also, we recommend using a hybrid approach that combines model checking with a variety of languages and semantic technologies in developing future IoT-based apps verification frameworks to cover all levels and types of conflicts to guarantee and increase the safety, security, and correctness of IoT systems.

Survey on Periodic Scheduling for Time-triggered Hard Real-time Systems

This survey covers the basic principles and related works addressing the time-triggered scheduling of periodic tasks with deadlines. The wide range of applications and the increasing complexity of modern real-time systems result in the continually growing interest in this topic. However, the articles in this field appear without systematic notation. To address it, we extend the three-field Graham notation to cover periodic scheduling. Moreover, we formally define three example periodic scheduling problems (PSPs) and provide straightforward implementations of these examples in the Satisfiability Modulo Theories formalism with source codes. Then, we present a summary of the complexity results containing existing polynomially solvable PSPs. We also provide an overview of simple state-of-the-art methods and tricks to solve the PSPs efficiently in terms of time. Next, we survey the existing works on PSP according to the resource environment: scheduling on a single resource, on parallel identical resources, and on dedicated resources. In the survey, we indicate which works propose solution methods for more general PSPs. Finally, we present related problems that are not periodic by nature to provide inspiration for the PSP solution.