Concurrent incorrectness separation logic

Incorrectness separation logic (ISL) was recently introduced as a theory of under-approximate reasoning, with the goal of proving that compositional bug catchers find actual bugs. However, ISL only considers sequential programs. Here, we develop concurrent incorrectness separation logic (CISL), which extends ISL to account for bug catching in concurrent programs. Inspired by the work on Views, we design CISL as a parametric framework, which can be instantiated for a number of bug catching scenarios, including race detection, deadlock detection, and memory safety error detection. For each instance, the CISL meta-theory ensures the soundness of incorrectness reasoning for free, thereby guaranteeing that the bugs detected are true positives.

Symbolic and Structural Model-Checking

Brute-force model-checking consists in exhaustive exploration of the state-space of a Petri net, and meets the dreaded state-space explosion problem. In contrast, this paper shows how to solve model-checking problems using a combination of techniques that stay in complexity proportional to the size of the net structure rather than to the state-space size. We combine an SMT based over-approximation to prove that some behaviors are unfeasible, an under-approximation using memory-less sampling of runs to find witness traces or counter-examples, and a set of structural reduction rules that can simplify both the system and the property. This approach was able to win by a clear margin the model-checking contest 2020 for reachability queries as well as deadlock detection, thus demonstrating the practical effectiveness and general applicability of the system of rules presented in this paper.

Deadlock detection in distributed system

In highly automated devices, deadlock is a case that occurs when no system can permit its event which may give irrelevant economic losses. A process can request or release resources that are either available or are on hold by others. If a process requesting a resource is not available at any time, then that process enters into the waiting state. But if a waiting state is not converted into its present state, it enters more than two processes are having an indefinite waiting state. The proposed algorithm gives an efficient way for deadlock detection. For the implementation of this work, C++ and python as the basic programming language are used. It gives an idea about how resources are allocated, and how few processes result in deadlock.

Robot coalition formation against time-extended multi-robot tasks

PurposeMulti-robot coalition formation (MRCF) refers to the formation of robot coalitions against complex tasks requiring multiple robots for execution. Situations, where the robots have to participate in multiple coalitions over time due to a large number of tasks, are called Time-extended MRCF. While being NP-hard, time-extended MRCF also holds the possibility of resource deadlocks due to any cyclic hold-and-wait conditions among the coalitions. Existing schemes compromise on solution quality to form workable, deadlock-free coalitions through instantaneous or incremental allocations.Design/methodology/approachThis paper presents an evolutionary algorithm (EA)-based task allocation framework for improved, deadlock-free solutions against time-extended MRCF. The framework simultaneously allocates multiple tasks, allowing the robots to participate in multiple coalitions within their schedule. A directed acyclic graph–based representation of robot plans is used for deadlock detection and avoidance.FindingsAllowing the robots to participate in multiple coalitions within their schedule, significantly improves the allocation quality. The improved allocation quality of the EA is validated against two auction schemes inspired by the literature.Originality/valueTo the best of the author's knowledge, this is the first framework which simultaneously considers multiple MR tasks for deadlock-free allocation while allowing the robots to participate in multiple coalitions within their plans.