We introduce the notion of local completeness in abstract interpretation and define a logic for proving both the correctness and incorrectness of some program specification. Abstract interpretation ...is extensively used to design sound-by-construction program analyses that over-approximate program behaviours. Completeness of an abstract interpretation A for all possible programs and inputs would be an ideal situation for verifying correctness specifications, because the analysis can be done compositionally and no false alert will arise. Our first result shows that the class of programs whose abstract analysis on A is complete for all inputs has a severely limited expressiveness. A novel notion of local completeness weakens the above requirements by considering only some specific, rather than all, program inputs and thus finds wider applicability. In fact, our main contribution is the design of a proof system, parameterized by an abstraction A, that, for the first time, combines over- and under-approximations of program behaviours. Thanks to local completeness, in a provable triple ⊢A P c Q, the assertion Q is an under-approximation of the strongest post-condition postc(P) such that the abstractions in A of Q and postc(P) coincide. This means that Q is never too coarse, namely, under mild assumptions, the abstract interpretation of c does not yield false alerts for the input P iff Q has no alert. Thus, ⊢A P c Q not only ensures that all the alerts raised in Q are true ones, but also that if Q does not raise alerts then c is correct.
Energy efficiency, real-time response, and data transmission reliability are important objectives during networked systems design. This paper aims to develop an efficient task mapping scheme to ...balance these important but conflicting objectives. To achieve this goal, tasks are triplicated to enhance reliability and mapped on the wireless nodes of the networked systems with Dynamic Voltage and Frequency Scaling (DVFS) capabilities to reduce energy consumption while still meeting real-time constraints. Our contributions include the mathematical formulation of this task mapping problem as mixed-integer programming that balances node energy consumption, enhancing data reliability, under real-time and energy constraints. Compared with the State-of-the-Art (SoA), a joint-design problem is considered in this paper, where DVFS, task triplication, task allocation, and task scheduling are optimized concurrently. To find the optimal solution, the original problem is linearized, and a decomposition-based method is proposed. The optimality of the proposed method is proved rigorously. Furthermore, a heuristic based on the greedy algorithm is designed to reduce the computation time. The proposed methods are evaluated and compared through a series of simulations. The results show that the proposed triplication-based task mapping method on average achieves 24.84% runtime reduction and 28.62% energy saving compared to the SoA methods.
Positive first-order logic on words Kuperberg, Denis
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS),
06/2021
Conference Proceeding
Odprti dostop
We study FO+, a fragment of first-order logic on finite words, where monadic predicates can only appear positively. We show that there is an FO-definable language that is monotone in monadic ...predicates but not definable in FO+. This provides a simple proof that Lyndon's preservation theorem fails on finite structures. We additionally show that given a regular language, it is undecidable whether it is definable in FO+.
In recent years, the number of devices and terminals connected to the smart city has increased significantly. Edge networks face a greater variety of connected objects and massive services. ...Considering that a large number of services have different QoS requirements, it has always been a huge challenge for smart city to optimally allocate limited computing resources to all services to obtain satisfactory performance. In particular, delay is intolerable for services in certain applications, such as medical, industrial applications, etc, that such applications require the high priority. Therefore, through flexibly dynamic scheduling, it is crucial to schedule services to the optimal node to ensure user experience. In this paper, we propose a resource allocation scheme for hierarchical edge computing network in smart city based on attention mechanism, for extracting a small number of features that can represent services from a large amount of information collected from edge nodes. The attention mechanism is used to quickly determine the priority of the services. Based on this, task deployment and resource allocation for different task priorities are developed to ensure the quality of service in smart cities by introducing Q-learning. Simulation results show that the proposed scheme can effectively improve the edge network resource utilization, reduce the average delay of task processing, and effectively guarantee the quality of service.
Concurrent Separation Logic Meets Template Games Melliès, Paul-André; Stefanesco, Léo
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science,
07/2020
Conference Proceeding
Odprti dostop
An old dream of concurrency theory and programming language semantics has been to uncover the fundamental synchronization mechanisms which regulate situations as different as game semantics for ...higher-order programs, and Hoare logic for concurrent programs with shared memory and locks. We establish a deep and unexpected connection between two recent lines of work on concurrent separation logic (CSL) and on template game semantics for differential linear logic (DiLL). Thanks to this connection, we reformulate in the purely conceptual style of template games for DiLL the asynchronous and interactive interpretation of CSL designed by Melliès and Stefanesco in a recent work. We believe that the analysis reveals something important about the secret anatomy of CSL, and more specifically about the subtle interplay, of a categorical nature, between sequential composition, parallel product, errors and locks.
The scheduling literature has traditionally focused on a single type of resource (e.g., computing nodes). However, scientific applications in modern High-Performance Computing (HPC) systems process ...large amounts of data, hence have diverse requirements on different types of resources (e.g., cores, cache, memory, I/O). All of these resources could potentially be exploited by the runtime scheduler to improve the application performance. In this paper, we study multi-resource scheduling to minimize the makespan of computational workflows comprised of parallel jobs subject to precedence constraints. The jobs are assumed to be moldable, allowing the scheduler to flexibly select a variable set of resources before execution. We propose a multi-resource, list-based scheduling algorithm, and prove that, on a system with d types of schedulable resources, our algorithm achieves an approximation ratio of for any d, and a ratio of for large d. We also present improved results for independent jobs and for jobs with special precedence constraints (e.g., series-parallel graphs and trees). Finally, we prove a lower bound of d on the approximation ratio of any list scheduling scheme with local priority considerations. To the best of our knowledge, these are the first approximation results for moldable workflows with multiple resource requirements.
In search of lost time Aceto, Luca; Anastasiadi, Elli; Castiglioni, Valentina ...
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS),
06/2021
Conference Proceeding
Odprti dostop
This survey reviews some of the most recent achievements in the saga of the axiomatisation of parallel composition, along with some classic results. We focus on the recursion, relabelling and ...restriction free fragment of CCS and we discuss the solutions to three problems that were open for many years. The first problem concerns the status of Bergstra and Klop's auxiliary operators left merge and communication merge in the finite axiomatisation of parallel composition modulo bisimiliarity: We argue that, under some natural assumptions, the addition of a single auxiliary binary operator to CCS does not yield a finite axiomatisation of bisimilarity. Then we delineate the boundary between finite and non-finite axiomatisability of the congruences in van Glabbeek's linear time-branching time spectrum over CCS. Finally, we present a novel result to the effect that rooted weak bisimilarity has no finite complete axiomatisation over CCS.
This paper proposes an energy-aware scheduling of malleable fork-join (MFJ) tasks on heterogeneous multicores. This work allows a task to be split into multiple sub-tasks for fork-join parallel ...execution. The number of the sub-tasks is determined simultaneously with scheduling. Our scheduling technique aims at the minimization of energy consumption under a deadline constraint. In addition, this paper proposes a technique for simultaneous scheduling and core-type optimization. The technique optimally decides types of cores (to be either "big" or "little") at the same time as MFJ task scheduling in order to further reduce energy consumption.
Distributed jobs typically facing competition for multiple resources in modern data centers, especially for network. Without effective network scheduling, this competition can cause low efficiency of ...the data center. Previous work on network scheduling has been focused on reducing flow completion time or improving per-flow fairness. Yet, its effect on improving jobs’ performance is limited by the unawareness of relationships between communication and computation. In this paper, we focus on the problem of scheduling network resources for multiple jobs, with the specific objective to reduce the job completion time (JCT), which also makes the datacenter more efficient. With an in-depth investigation of communication and computation, we identify an opportunity for accelerating jobs in a way that occupies less bandwidth for DAG-based complicated modern jobs. Accordingly, this paper proposes JIT, a job-aware network scheduler that leverages the computational graph to accelerate jobs effectively. To cater to the goal of JIT, we first develop a mathematical model and formulate the scheduling problem as an integer linear programming (ILP) problem. We further prove that it has an equivalent linear programming (LP) problem through rigorous theoretical analysis in order to solve this ILP problem efficiently. Some reasonable simplifications are also adopted to reduce the solving time of JIT to only 1 second. The proposed JIT is simulated and compared against some state-of-the-art designs, and the simulation results demonstrate that JIT can achieve an acceleration of up to 1.55 × , which successfully improves the efficiency of the data center.
Normalization for cubical type theory Sterling, Jonathan; Angiuli, Carlo
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS),
06/2021
Conference Proceeding
Odprti dostop
We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is ...reduction-free, in the sense of yielding a bijection between equivalence classes of terms in context and a tractable language of β/η-normal forms. As corollaries we obtain both decidability of judgmental equality and the injectivity of type constructors.
PDF
