اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدA Concurrent Language with a Uniform Treatment of Regions and Locks
95
0
0.0
(
0
)
تأليف
Prodromos Gerakios
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
A challenge for programming language research is to design and implement multi-threaded low-level languages providing static guarantees for memory safety and freedom from data races. Towards this goal, we present a concurrent language employing safe region-based memory management and hierarchical locking of regions. Both regions and locks are treated uniformly, and the language supports ownership transfer, early deallocation of regions and early release of locks in a safe manner.
قيم البحث
اقرأ أيضاً
We present a programming methodology and runtime performance case study comparing the declarative data flow coordination language S-Net with Intels Concurrent Collections (CnC). As a coordination language S-Net achieves a near-complete separation of
concerns between sequential software components implemented in a separate algorithmic language and their parallel orchestration in an asynchronous data flow streaming network. We investigate the merits of S-Net and CnC with the help of a relevant and non-trivial linear algebra problem: tiled Cholesky decomposition. We describe two alternative S-Net implementations of tiled Cholesky factorization and compare them with two CnC implementations, one with explicit performance tuning and one without, that have previously been used to illustrate Intel CnC. Our experiments on a 48-core machine demonstrate that S-Net manages to outperform CnC on this problem.
Objects and actors are communicating state machines, offering and consuming different services at different points in their lifecycle. Two complementary challenges arise when programming such systems. When objects interact, their state machines must
be compatible, so that services are requested only when they are available. Dually, when objects refine other objects, their state machines must be compliant, so that services are honoured whenever they are promised. In this paper we show how the idea of multiparty compatibility from the session types literature can be applied to both of these problems. We present an untyped language in which concurrent objects are checked automatically for compatibility and compliance. For simple objects, checking can be exhaustive and has the feel of a type system. More complex objects can be partially validated via test cases, leading to a methodology closer to continuous testing. Our proof-of-concept implementation is limited in some important respects, but demonstrates the potential value of the approach and the relationship to existing software development practices.
We define a domain-specific language (DSL) to inductively assemble flow networks from small networks or modules to produce arbitrarily large ones, with interchangeable functionally-equivalent parts. Our small networks or modules are small only as the
building blocks in this inductive definition (there is no limit on their size). Associated with our DSL is a type theory, a system of formal annotations to express desirable properties of flow networks together with rules that enforce them as invariants across their interfaces, i.e, the rules guarantee the properties are preserved as we build larger networks from smaller ones. A prerequisite for a type theory is a formal semantics, i.e, a rigorous definition of the entities that qualify as feasible flows through the networks, possibly restricted to satisfy additional efficiency or safety requirements. This can be carried out in one of two ways, as a denotational semantics or as an operational (or reduction) semantics; we choose the first in preference to the second, partly to avoid exponential-growth rewriting in the operational approach. We set up a typing system and prove its soundness for our DSL.
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.
While modern software development heavily uses versioned packages, programming languages rarely support the concept
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
