The Experts below are selected from a list of 360 Experts worldwide ranked by ideXlab platform

Marcel Oliveira - One of the best experts on this subject based on the ideXlab platform.

  • a refinement checking based strategy for component based systems evolution
    Journal of Systems and Software, 2020
    Co-Authors: Jose Dihego, Augusto Sampaio, Marcel Oliveira
    Abstract:

    Abstract We propose inheritance and refinement relations for a CSP-based component model ( BRIC ), which supports a constructive design based on composition rules that preserve classical concurrency properties such as Deadlock Freedom. The proposed relations allow extension of functionality, whilst preserving behavioural properties. A notion of extensibility is defined on top of a behavioural relation called convergence, which distinguishes inputs from outputs and the context where they are communicated, allowing extensions to reuse existing events with different purposes. We mechanise the strategy for extensibility verification using the FDR4 tool, and illustrate our results with an autonomous healthcare robot case study.

Marco Bernardo - One of the best experts on this subject based on the ideXlab platform.

  • a general approach to Deadlock Freedom verification for software architectures
    Lecture Notes in Computer Science, 2003
    Co-Authors: Alessandro Aldini, Marco Bernardo
    Abstract:

    When building complex software systems, the designer is faced with the problem of detecting mismatches arising from the activity of assembling components. The adoption of formal methods becomes unavoidable in order to support a precise identification of such mismatches in the early design stages. As far as Deadlock Freedom is concerned, some techniques appeared in the literature, which apply to formal specifications of software architectures under some constraints. In this paper we develop a novel technique for Deadlock Freedom verification that can be applied to arbitrary software architectures, thus overcoming the limitations of the previous techniques.

Tushar Krishna - One of the best experts on this subject based on the ideXlab platform.

  • bindu Deadlock Freedom with one bubble in the network
    Networks-on-Chips, 2019
    Co-Authors: Mayank Parasar, Tushar Krishna
    Abstract:

    Every interconnection network must ensure, for its functional correctness, that it is Deadlock free. A routing Deadlock occurs when there is a cyclic dependency of packets when acquiring the buffers of the routers. Prior solutions have provisioned an extra set of escape buffers to resolve Deadlocks, or restrict the path that a packet can take in the network by disallowing certain turns. This either pays higher power/area overhead or impacts performance. In this work, we demonstrate that (i) keeping one virtual-channel in the entire network (called 'Bindu') empty, and (ii) forcing it to move through all input ports of every router in the network via a pre-defined path, can guarantee Deadlock-Freedom. We show that our scheme (a) is topology agnostic (we evaluate it on multiple topologies, both regular and irregular), (b) does not impose any turn restrictions on packets, (c) does not require an extra set of escape buffers, and (d) is free from the complex circuitry for detecting and recovering from Deadlocks. We report 15% average improvement in throughput for synthetic traffic and 7% average reduction in runtime for real applications over state-of-the-art Deadlock Freedom schemes.

  • synchronized progress in interconnection networks spin a new theory for Deadlock Freedom
    IEEE Micro, 2019
    Co-Authors: Aniruddh Ramrakhyani, Paul V Gratz, Tushar Krishna
    Abstract:

    Routing Deadlocks, i.e., a cyclic dependence between buffered packets, are a fundamental network design challenge. Existing solutions require resource over provisioning. We propose a new theory for Deadlock Freedom, Synchronized Progress in Interconnection Networks (SPIN) that solves the problem through coordinated movement of Deadlocked packets.

  • brownian bubble router enabling Deadlock Freedom via guaranteed forward progress
    Networks-on-Chips, 2018
    Co-Authors: Mayank Parasar, Ankit Sinha, Tushar Krishna
    Abstract:

    Deadlocks are a bane for network designers, be it a Network on Chip (NoC) in a multi-core or a large scale HPC/datacenter network. A routing Deadlock occurs when there is a cyclic dependence between the buffers of network routers. Most modern systems avoid Deadlocks by placing routing restrictions or adding extra virtual channels, in turn hurting performance and adding overhead respectively. In this work, we demonstrate that instead of placing such restrictions, we can, in fact, design routers to themselves guarantee Deadlock-Freedom, by (i) ensuring that every router always has at least one bubble (i.e., free buffer slot) at any input port, and (ii) this bubble pro-actively moves between input ports. We call this a Brownian Bubble Router (BBR). A BBR guarantees forward progress in any network topology, without requiring any routing restrictions or additional virtual channels. With our BBR design we provide 4× better throughput over state of art Deadlock recovery schemes and 40% better throughput over traditional Deadlock avoidance schemes in a 8×8 Mesh at negligible area and power overheads.

  • synchronized progress in interconnection networks spin a new theory for Deadlock Freedom
    International Symposium on Computer Architecture, 2018
    Co-Authors: Aniruddh Ramrakhyani, Paul V Gratz, Tushar Krishna
    Abstract:

    One of the most fundamental design challenges in any interconnection network is that of routing Deadlocks. A Deadlock is a cyclic dependence between buffers that renders forward progress impossible. Deadlocks are a necessary evil and almost every on-chip/HPC network today avoids it either via routing restrictions across physical channels (Daily's Theory) or with at least one escape virtual channel (Duato's Theory). This ensures that a cyclic dependence between buffers is never created in the first place. Moreover, each solution is tied to a specific topology, requiring an updated policy if the topology were to change. Alternately, solutions have also been proposed to reserve certain resources (buffers) and allocate them only upon detection of a Deadlock, thereby breaking the dependence chain and recovering from the Deadlock. Unfortunately, all these approaches fundamentally lead to a loss in available bandwidth due to routing restrictions or buffer resource usage restrictions. In this work, we challenge the theoretical notion of viewing Deadlocks as a lack of routing resource (buffers) problem that every solution to date is based on. We argue that a Deadlock can in fact be considered as a lack of coordination between distributed entities. We prove that orchestrating a forward movement of every flit in the Deadlocked ring at exactly the same time, which we call a spin, can guarantee forward progress and eventually lead to Deadlock resolution with a bounded number of spins. We name this novel theory as SPIN (Synchronized Progress in Interconnection Networks). SPIN eliminates the need for virtual channels to achieve Deadlock Freedom thereby enabling fully adaptive routing with only one buffer per message class. We illustrate this capability by designing FAvORS, a novel truly one VC fully-adaptive routing algorithm. We also present a low-cost distributed implementation of SPIN and compare it against state-of-the-art Deadlock avoidance/recovery schemes. SPIN provides up to 80% higher throughput, 52% lower area and 50% lower power for an on-chip 64-core mesh, and up to 83% higher throughput, 53% lower area and 55% lower power for an off-chip 1024-node dragon-fly.

Hana Chockler - One of the best experts on this subject based on the ideXlab platform.

  • efficiently verifiable conditions for Deadlock Freedom of large concurrent programs
    Lecture Notes in Computer Science, 2005
    Co-Authors: Paul C Attie, Hana Chockler
    Abstract:

    We present two polynomial-time algorithms for automatic verification of Deadlock-Freedom of large finite-state concurrent programs. We consider shared-memory concurrent programs in which a process can nondeterministically choose amongst several (enabled) actions at any step. As shown in [23], Deadlock-Freedom analysis is NP-hard even for concurrent programs of restricted form (no nondeterministic choice). Therefore, research in this area concentrates either on the search for efficiently checkable sufficient conditions for Deadlock-Freedom, or on improving the complexity of the check in some special cases. In this paper, we present two efficiently checkable sufficient conditions for Deadlock Freedom. Our algorithms apply to programs which are expressed in a particular syntactic form, in which variables are shared between pairs of processes. The first algorithm improves the complexity of the Deadlock check of Attie and Emerson [4] to polynomial in all parameters, as opposed to the exponential complexity of [4]. The second algorithm involves a conceptually new construction of a global wait-for graph for all processes. Its running time is also polynomial in all its parameters, and it is more discriminating than the first algorithm. We illustrate our algorithms by applying them to several examples of concurrent programs that implement resource allocation and priority queues. To the best of our knowledge, this is the first work that describes polynomially checkable conditions for assuring Deadlock Freedom of large concurrent programs.

Rajagopal Nagarajan - One of the best experts on this subject based on the ideXlab platform.

  • a specification structure for Deadlock Freedom of synchronous processes
    Theoretical Computer Science, 1999
    Co-Authors: Samson Abramsky, Rajagopal Nagarajan
    Abstract:

    Many different notions of “program property”, and many different methods of verifying such properties, arise naturally in programming. We present a general framework of Specification Structures for combining different notions and methods in a coherent fashion. We then apply the idea of specification structures to concurrency in the setting of Interaction Categories. As a specific example, a certain specification structure defined over the interaction category GProc yields a new category GProcD in which morphisms are Deadlock-free concurrent processes and composition is process interaction. GProcD is obtained from GProc by adding specification information to the objects which is strong enough to guarantee Deadlock-Freedom. The main technical contribution is to show that this can be done in a way which is preserved by composition. The methods used to achieve this can be seen as a semantic analogue of those used to prove strong normalization in classical linear logic.

  • a type theoretic approach to Deadlock Freedom of asynchronous systems
    International Symposium on Theoretical Aspects of Computer Software, 1997
    Co-Authors: Samson Abramsky, Rajagopal Nagarajan
    Abstract:

    We present a type-based technique for the verification of Deadlock-Freedom in asynchronous concurrent systems. Our general approach is to start with a simple interaction category, in which objects are types containing safety specifications and morphisms are processes. We then use a specification structure to add information to the types so that they specify stronger properties. In this paper the starting point is the category ASProc and the extra type information concerns Deadlock-Freedom. In the resulting category ASPrOC D , combining well-typed processes preserves Deadlock-Freedom. It is also possible to accommodate non-compositional methods within the same framework. The systems we consider are asynchronous, hence issues of divergence become significant; our approach incorporates an elegant treatment of both divergence and successful termination. As an example, we use our methods to verify the Deadlock-Freedom of an implementation of the alternating-bit protocol.