Type Inference for Deadlock Detection in a Multithreaded Polymorphic Typed Assembly Language

We previously developed a polymorphic type system and a type checker for a multithreaded lock-based polymorphic typed assembly language (MIL) that ensures that well-typed programs do not encounter race conditions. This paper extends such work by taking into consideration deadlocks. The extended type...

Full description

Bibliographic Details
Main Authors: Vasco T. Vasconcelos, Francisco Martins, Tiago Cogumbreiro
Format: Article
Language:English
Published: Open Publishing Association 2010-02-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1002.0942v2
_version_ 1811299005769973760
author Vasco T. Vasconcelos
Francisco Martins
Tiago Cogumbreiro
author_facet Vasco T. Vasconcelos
Francisco Martins
Tiago Cogumbreiro
author_sort Vasco T. Vasconcelos
collection DOAJ
description We previously developed a polymorphic type system and a type checker for a multithreaded lock-based polymorphic typed assembly language (MIL) that ensures that well-typed programs do not encounter race conditions. This paper extends such work by taking into consideration deadlocks. The extended type system verifies that locks are acquired in the proper order. Towards this end we require a language with annotations that specify the locking order. Rather than asking the programmer (or the compiler's backend) to specifically annotate each newly introduced lock, we present an algorithm to infer the annotations. The result is a type checker whose input language is non-decorated as before, but that further checks that programs are exempt from deadlocks.
first_indexed 2024-04-13T06:28:44Z
format Article
id doaj.art-f504cfaaa15f49f1b14eea4b292b9343
institution Directory Open Access Journal
issn 2075-2180
language English
last_indexed 2024-04-13T06:28:44Z
publishDate 2010-02-01
publisher Open Publishing Association
record_format Article
series Electronic Proceedings in Theoretical Computer Science
spelling doaj.art-f504cfaaa15f49f1b14eea4b292b93432022-12-22T02:58:19ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802010-02-0117Proc. PLACES 20099510910.4204/EPTCS.17.8Type Inference for Deadlock Detection in a Multithreaded Polymorphic Typed Assembly LanguageVasco T. VasconcelosFrancisco MartinsTiago CogumbreiroWe previously developed a polymorphic type system and a type checker for a multithreaded lock-based polymorphic typed assembly language (MIL) that ensures that well-typed programs do not encounter race conditions. This paper extends such work by taking into consideration deadlocks. The extended type system verifies that locks are acquired in the proper order. Towards this end we require a language with annotations that specify the locking order. Rather than asking the programmer (or the compiler's backend) to specifically annotate each newly introduced lock, we present an algorithm to infer the annotations. The result is a type checker whose input language is non-decorated as before, but that further checks that programs are exempt from deadlocks.http://arxiv.org/pdf/1002.0942v2
spellingShingle Vasco T. Vasconcelos
Francisco Martins
Tiago Cogumbreiro
Type Inference for Deadlock Detection in a Multithreaded Polymorphic Typed Assembly Language
Electronic Proceedings in Theoretical Computer Science
title Type Inference for Deadlock Detection in a Multithreaded Polymorphic Typed Assembly Language
title_full Type Inference for Deadlock Detection in a Multithreaded Polymorphic Typed Assembly Language
title_fullStr Type Inference for Deadlock Detection in a Multithreaded Polymorphic Typed Assembly Language
title_full_unstemmed Type Inference for Deadlock Detection in a Multithreaded Polymorphic Typed Assembly Language
title_short Type Inference for Deadlock Detection in a Multithreaded Polymorphic Typed Assembly Language
title_sort type inference for deadlock detection in a multithreaded polymorphic typed assembly language
url http://arxiv.org/pdf/1002.0942v2
work_keys_str_mv AT vascotvasconcelos typeinferencefordeadlockdetectioninamultithreadedpolymorphictypedassemblylanguage
AT franciscomartins typeinferencefordeadlockdetectioninamultithreadedpolymorphictypedassemblylanguage
AT tiagocogumbreiro typeinferencefordeadlockdetectioninamultithreadedpolymorphictypedassemblylanguage