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...
Main Authors: | , , |
---|---|
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 |