Concurrent object-oriented programminglanguages coordinate conflicting memory accesses through locking, which relies on programmer discipline and suffers from a lack of modularity and compile-time support. Programmer...
详细信息
ISBN:
(纸本)9783642370366
Concurrent object-oriented programminglanguages coordinate conflicting memory accesses through locking, which relies on programmer discipline and suffers from a lack of modularity and compile-time support. Programmers typically work with large libraries of code whose locking behaviours are not formally and precisely specified;thus understanding and writing concurrent programs is notoriously difficult and error-prone. This paper proposes structural lock correlation, a new model for establishing structural connections between locks and the memory locations they protect, in an ownership-based type and effect system. Structural lock correlation enables modular specification of locking. It offers a compiler-checkable lock abstraction with an enforceable contract at interface boundaries, leading to improved safety, understandability and composability of concurrent program components.
Recursive functions defined on a coalgebraic datatype C may not converge if there are cycles in the input, that is, if the input object is not well-founded. Even so, there is often a useful solution. Unfortunately, cu...
详细信息
ISBN:
(纸本)9783642370366
Recursive functions defined on a coalgebraic datatype C may not converge if there are cycles in the input, that is, if the input object is not well-founded. Even so, there is often a useful solution. Unfortunately, current functional programminglanguages provide no support for specifying alternative solution methods. In this paper we give numerous examples in which it would be useful to do so: free variables, alpha-conversion, and substitution in infinitary lambda-terms;halting probabilities and expected running times of probabilistic protocols;abstract interpretation;and constructions involving finite automata. In each case the function would diverge under the standard semantics of recursion. We propose programming language constructs that would allow the specification of alternative solutions and methods to compute them.
We present Why3, a tool for deductive program verification, and WhyML, its programming and specification language. WhyML is a first-order language with polymorphic types, pattern matching, and inductive predicates. Pr...
详细信息
ISBN:
(纸本)9783642370366
We present Why3, a tool for deductive program verification, and WhyML, its programming and specification language. WhyML is a first-order language with polymorphic types, pattern matching, and inductive predicates. Programs can make use of record types with mutable fields, type invariants, and ghost code. Verification conditions are discharged by Why3 with the help of various existing automated and interactive theorem provers. To keep verification conditions tractable and comprehensible, WhyML imposes a static control of aliases that obviates the use of a memory model. A user can write WhyML programs directly and get correct-by-construction OCaml programs via an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. We demonstrate the benefits of Why3 and WhyML on non-trivial examples of program verification.
It is known that model checkers can generate test inputs as witnesses for reachability specifications (or, equivalently, as counterexamples for safety properties). While this use of model checkers for testing yields a...
详细信息
ISBN:
(纸本)9783642370366
It is known that model checkers can generate test inputs as witnesses for reachability specifications (or, equivalently, as counterexamples for safety properties). While this use of model checkers for testing yields a theoretically sound test-generation procedure, it scales poorly for computing complex test suites for large sets of test goals, because each test goal requires an expensive run of the model checker. We represent test goals as automata and exploit relations between automata in order to reuse existing reachability information for the analysis of subsequent test goals. Exploiting the sharing of sub-automata in a series of reachability queries, we achieve considerable performance improvements over the standard approach. We show the practical use of our multi-goal reachability analysis in a predicate-abstraction-based test-input generator for the test-specification language FQL.
The proceedings contain 7 papers. The topics discussed include: checking process-oriented operating system behavior using CSP and refinement;a microkernel API for fine-grained decomposition;code-partitioning gossip;ca...
ISBN:
(纸本)9781605588445
The proceedings contain 7 papers. The topics discussed include: checking process-oriented operating system behavior using CSP and refinement;a microkernel API for fine-grained decomposition;code-partitioning gossip;catchandretry: extending exceptions to handle distributed system failures and recovery;filet-o-fish: practical and dependable domain-specific languages for OS development;Kstruct: preserving consistency through c annotations;and distributed data flow language for multi-party protocols.
This paper presents a novel object-oriented approach to modeling the semantics of distributed multi-party protocols such as leader election, distributed locks or reliable multicast, and a programming language that sup...
详细信息
We address a persistent problem with using domain-specific languages to write operating systems: the effort of implementing, checking, and debugging the DSL usually outweighs any of its benefits. Because these DSLs ge...
详细信息
Multiple petascale systems will soon be available to the computational science community and will represent a variety of architectural models. These high-endsystems, like all computing platforms, will have an increas...
详细信息
ISBN:
(纸本)9781424416936
Multiple petascale systems will soon be available to the computational science community and will represent a variety of architectural models. These high-endsystems, like all computing platforms, will have an increasing C, reliance on software-managed on-chip parallelism. These architectural trends brine, into question the message, passing programming model that has dominated high-endprogramming for the past decade. In this talk I will describe some of the technology challenges that will drive the design of future systems and their implications for software tools, algorithm design, and application programming. In particular, I will show a need to consider models other than message passing as we move towards massive on-chip parallelism. I will talk about a class of Partitioned Global Address Space (PGAS) languages, which are an alternative to both message passing models like MPI and shared memory models like OpenMP. PGAS languages offer the possibility of a programming model that will work well across a wide range of shared memory, distributed memory, and hybrid platforms. Some of these languages, including UPC, CAF and Titanium, are based on a static model of parallelism, which gives programmers direct control over the underlying processor resources. The restricted nature of the static parallelism model in these languages has advantages in terms of implementation simplicity, analyzability, and performance transparency, but some applications demand a more dynamic execution model, similar to that of Charm++ or the recently developed HPCS languages (X10, Chapel, and Fortress). I will describe some of our experience working with both static and dynamically managed applications and some of the research challenges that I believe will be critical in developing viable programming techniques for future systems.
As high-end computer systems present users with rapidly increasing numbers of processors, possibly also incorporating attached co-processors, programmers are increasingly challenged to express the necessary levels of ...
详细信息
ISBN:
(纸本)9781424416936
As high-end computer systems present users with rapidly increasing numbers of processors, possibly also incorporating attached co-processors, programmers are increasingly challenged to express the necessary levels of concurrency with the dominant parallel programming model, Fortran+MPI+OpenMP (or minor variations). In this paper, we examine the languages developed under the DARPA High-Productivity Computing systems (HPCS) program (Chapel, Fortress, and X10) as representatives of a different parallel programming model which might be more effective on emerging high-performance systems. The application used in this study is the Hartree-Fock method from quantum chemistry, which combines access to distributed data with a task-parallel algorithm and is characterized by significant irregularity in the computational tasks. We present several different implementation strategies for load balancing of the task-parallel computation, as well as distributed array operations, in each of the three languages. We conclude that the HPCS languages provide a wide variety of mechanisms for expressing parallelism, which can be combined at multiple levels, making them quite expressive for this problem.
暂无评论