This paper provides a true-concurrency approach for the specification and verification of systems of concurrent communicating agents with durable actions. We present high-level Petri nets with durable actions (DaHL) to cope with various details in such complex systems. We define a DaHL module as an open variant of time-dependent colored Petri nets. A DaHL system is a fused set of modules for systems consisting of concurrent agents which can interact with each other. We also introduce hybrid-based reachability graph that covers the entire state space of DaHL systems with a true-concurrency semantics. We show that such reachability graph allows us to check important properties such as deadlock-freeness, liveness, home space, and reversibility, and also to predict timing properties prior to real implementation. A case study is used to model and analyze a simple scenario where autonomous vehicles are able to transport containers freely in an enterprise environment.
The paper presents an approach to the design and implementation of web-based environments for practical exercises in parallel and distributed computing (PDC). The presented approach introduces minimal development and operational costs by relying on Everest, a general-purpose platform for building computational web services. The flexibility of proposed service-oriented architecture enables the development of different types of services targeting various use cases and PDC topics. The generic execution services support the execution of different types of parallel and distributed programs on corresponding computing systems, while the assignment evaluation services implement the execution and evaluation of solutions to programming assignments. As was demonstrated by teaching two introductory PDC courses, the presented approach helps to enhance students’ practical experience while avoiding low-level interfaces, reducing the grading time and providing a level of automation necessary for scaling the course to a large number of students. In contrast to other efforts, the exploited Platform as a Service model provides the ability to quickly reuse this approach by other PDC educators without installation of the Everest platform.
Packet processing increasingly involves heterogeneous requirements. We consider the well-known model of a shared memory switch with bounded-size buffer and generalize it in two directions. First, we consider unit-sized packets labeled with an output port and a processing requirement (i.e., packets with heterogeneous processing), maximizing the number of transmitted packets. We analyze the performance of buffer management policies under various characteristics via competitive analysis that provides uniform guarantees across traffic patterns (Borodin and ElYaniv 1998). We propose the Longest-Work-Drop policy and show that it is at most 2-competitive and at least -competitive. Second, we consider another generalization, posed as an open problem in Goldwasser (2010), where each unit-sized packet is labeled with an output port and intrinsic value, and the goal is to maximize the total value of transmitted packets. We show first results in this direction and define a scheduling policy that, as we conjecture, may achieve constant competitive ratio. We also present a comprehensive simulation study that validates our results.
The main results of this paper are based on the idea that most load balancing algorithms can be described in the framework of optimization theory. It enables to involve classical results linked with convergence, its speed and other elements. We emphasize that these classical results have been found independently and till now this connection has not been shown clearly. In this paper, we analyze the load balancing algorithm based on the steepest descent algorithm. The analysis shows that the speed of convergence is determined by eigenvalues of the Laplacian for the graph of a given load balancing system. This consideration also leads to the problems of choosing an optimal structure for a load balancing system. We prove that these optimal graphs have special Laplacians: the multiplicities of their minimal and maximal positive eigenvalues must be greater than one. Such a property is essential for strongly regular graphs, investigated in algebraic graph theory.