Publication

Deadlock Detector for Synchronous Java.

Claude Petitpierre
2004
Reports

Abstract

In this paper, we present a work that aims to detect deadlocks in the programs written in the Synchronous Java language (sJava). It is based on an extension to a model-checking framework Bogor that allows the verification of concurrent Java programs. The deadlock detector allows developers to analyze the concurrent interaction of threads of active objects for searching all the reachable states and possible execution paths and detecting any deadlocks presented in a model. We propose in this work a solution that solves the problem of synchronization of method calls between active threads without using the traditional wait-notify mechanism. We also propose a utility that shows the graph of finite state machines of the simple models after verifying using Bogor.

Official source

https://infoscience.epfl.ch/entities/publication/f9959bf8-8d01-413a-bc07-acd8d22cb731

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Claude Petitpierre
2004
Reports

Abstract

Official source

https://infoscience.epfl.ch/entities/publication/f9959bf8-8d01-413a-bc07-acd8d22cb731

About this result

Related concepts (32)

Concurrent computing

Concurrent computing is a form of computing in which several computations are executed concurrently—during overlapping time periods—instead of sequentially—with one completing before the next starts. This is a property of a system—whether a program, computer, or a network—where there is a separate execution point or "thread of control" for each process. A concurrent system is one where a computation can advance without waiting for all other computations to complete. Concurrent computing is a form of modular programming.

Finite-state machine

A finite-state machine (FSM) or finite-state automaton (FSA, plural: automata), finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number of states at any given time. The FSM can change from one state to another in response to some inputs; the change from one state to another is called a transition. An FSM is defined by a list of its states, its initial state, and the inputs that trigger each transition.

Deadlock

In concurrent computing, deadlock is any situation in which no member of some group of entities can proceed because each waits for another member, including itself, to take action, such as sending a message or, more commonly, releasing a lock. Deadlocks are a common problem in multiprocessing systems, parallel computing, and distributed systems, because in these contexts systems often use software or hardware locks to arbitrate shared resources and implement process synchronization.

Related publications (4)

Deadlock Detector for Synchronous Java.

Chat with Graph Search

Digital Design with Implicit State Machines

Runtime Checking for Separation Logic

The LEAF Platform: Incremental Enhancements for the J2EE