Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA Type System for Unstructured Locking that Guarantees Deadlock Freedom without Imposing a Lock Ordering
113
0
0.0
(
0
)
Added by
EPTCS
Publication date
2011
fields
Informatics Engineering
and research's language is
English
Authors
Prodromos Gerakios
Ask ChatGPT about the research
No Arabic abstract
Deadlocks occur in concurrent programs as a consequence of cyclic resource acquisition between threads. In this paper we present a novel type system that guarantees deadlock freedom for a language with references, unstructured locking primitives, and locks which are implicitly associated with references. The proposed type system does not impose a strict lock acquisition order and thus increases programming language expressiveness.
rate research
Read More
Dynamic languages like Erlang, Clojure, JavaScript, and E adopted data-race freedom by design. To enforce data-race freedom, these languages either deep copy objects during actor (thread) communication or proxy back to their owning thread. We present Dala, a simple programming model that ensures data-race freedom while supporting efficient inter-thread communication. Dala is a dynamic, concurrent, capability-based language that relies on three core capabilities: immutable values can be shared freely; isolated mutable objects can be transferred between threads but not aliased; local objects can be aliased within their owning thread but not dereferenced by other threads. Objects with capabilities can co-exist with unsafe objects, that are unchecked and may suffer data races, without compromising the safety of safe objects. We present a formal model of Dala, prove data race-freedom and state and prove a dynamic gradual guarantee. These theorems guarantee data race-freedom when using safe capabilities and show that the addition of capabilities is semantics preserving modulo permission and cast errors.
Object-oriented scripting languages such as JavaScript or Python gain in popularity due to their flexibility. Still, the growing code bases written in the languages call for methods that make possible to automatically control the properties of the programs that ensure their stability in the running time. We propose a type system, called Lucretia, that makes possible to control the object structure of languages with reflection. Subject reduction and soundness of the type system with respect to the semantics of the language is proved.
Classes of set functions along with a choice of ground set are a bedrock to determine and develop corresponding variants of greedy algorithms to obtain efficient solutions for combinatorial optimization problems. The class of approximate constrained submodular optimization has seen huge advances at the intersection of good computational efficiency, versatility and approximation guarantees while exact solutions for unconstrained submodular optimization are NP-hard. What is an alternative to situations when submodularity does not hold? Can efficient and globally exact solutions be obtained? We introduce one such new frontier: The class of quasi-concave set functions induced as a dual class to monotone linkage functions. We provide a parallel algorithm with a time complexity over $n$ processors of $mathcal{O}(n^2g) +mathcal{O}(log{log{n}})$ where $n$ is the cardinality of the ground set and $g$ is the complexity to compute the monotone linkage function that induces a corresponding quasi-concave set function via a duality. The complexity reduces to $mathcal{O}(gnlog(n))$ on $n^2$ processors and to $mathcal{O}(gn)$ on $n^3$ processors. Our algorithm provides a globally optimal solution to a maxi-min problem as opposed to submodular optimization which is approximate. We show a potential for widespread applications via an example of diverse feature subset selection with exact global maxi-min guarantees upon showing that a statistical dependency measure called distance correlation can be used to induce a quasi-concave set function.
Context-Oriented Programming (COP) is a programming paradigm to encourage modularization of context-dependent software. Key features of COP are layers---modules to describe context-dependent behavioral variations of a software system---and their dynamic activation, which can modify the behavior of multiple objects that have already been instantiated. Typechecking programs written in a COP language is difficult because the activation of a layer can even change objects interfaces. Inoue et al. have informally discussed how to make JCop, an extension of Java for COP by Appeltauer et al., type-safe. In this article, we formalize a small COP language called ContextFJ$_{<:}$ with its operational semantics and type system and show its type soundness. The language models main features of the type-safe version of JCop, including dynamically activated first-class layers, inheritance of layer definitions, layer subtyping, and layer swapping.
Obtaining good performance when programming heterogeneous computing platforms poses significant challenges. We present a program transformation environment, implemented in Haskell, where architecture-agnostic scientific C code with semantic annotations is transformed into functionally equivalent code better suited for a given platform. The transformation steps are represented as rules that can be fired when certain syntactic and semantic conditions are fulfilled. These rules are not hard-wired into the rewriting engine: they are written in a C-like language and are automatically processed and incorporated into the rewriting engine. That makes it possible for end-users to add their own rules or to provide sets of rules that are adapted to certain specific domains or purposes.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
