GLORIA

GEOMAR Library Ocean Research Information Access

X

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
  • 1
    Online Resource
    Online Resource
    Race Detection in Two Dimensions
    Association for Computing Machinery (ACM) ; 2017
    In:  ACM Transactions on Parallel Computing Vol. 4, No. 4 ( 2017-12-31), p. 1-22
    Details
    In: ACM Transactions on Parallel Computing, Association for Computing Machinery (ACM), Vol. 4, No. 4 ( 2017-12-31), p. 1-22
    Abstract: Dynamic race detection is a program analysis technique for detecting errors caused by undesired interleavings of concurrent tasks. A primary challenge when designing efficient race detection algorithms is to achieve manageable space requirements. State-of-the-art algorithms for unstructured parallelism require Θ ( n ) space per monitored memory location, where n is the total number of tasks. This is a serious drawback when analyzing programs with many tasks. In contrast, algorithms for programs with a series-parallel (SP) structure require only Θ (1) space. Unfortunately, it is currently not well understood if there are classes of parallelism beyond SP that can also benefit from and be analyzed with Θ (1) space complexity. In this work, we show that structures richer than SP graphs, namely, that of two-dimensional (2D) lattices, can also be analyzed in Θ (1) space. Toward that (a) we extend Tarjan’s algorithm for finding lowest common ancestors to handle 2D lattices; (b) from that extension we derive a serial algorithm for race detection that can analyze arbitrary task graphs with a 2D lattice structure; (c) we present a restriction to fork-join that admits precisely the 2D lattices as task graphs (e.g., it can express pipeline parallelism). Our work generalizes prior work on structured race detection and aims to provide a deeper understanding of the interplay between structured parallelism and program analysis efficiency.
    Type of Medium: Online Resource
    ISSN: 2329-4949 , 2329-4957
    URL: Article
    DOI: 10.1145/3264618
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2017
    detail.hit.zdb_id: 2845845-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 2
    Online Resource
    Online Resource
    A practical construction for decomposing numerical abstract domains
    Association for Computing Machinery (ACM) ; 2018
    In:  Proceedings of the ACM on Programming Languages Vol. 2, No. POPL ( 2018-01), p. 1-28
    Details
    In: Proceedings of the ACM on Programming Languages, Association for Computing Machinery (ACM), Vol. 2, No. POPL ( 2018-01), p. 1-28
    Abstract: Numerical abstract domains such as Polyhedra, Octahedron, Octagon, Interval, and others are an essential component of static program analysis. The choice of domain offers a performance/precision tradeoff ranging from cheap and imprecise (Interval) to expensive and precise (Polyhedra). Recently, significant speedups were achieved for Octagon and Polyhedra by manually decomposing their transformers to work with the Cartesian product of projections associated with partitions of the variable set. While practically useful, this manual process is time consuming, error-prone, and has to be applied from scratch for every domain. In this paper, we present a generic approach for decomposing the transformers of sub-polyhedra domains along with conditions for checking whether the decomposed transformers lose precision with respect to the original transformers. These conditions are satisfied by most practical transformers, thus our approach is suitable for increasing the performance of these transformers without compromising their precision. Furthermore, our approach is ``black box:'' it does not require changes to the internals of the original non-decomposed transformers or additional manual effort per domain. We implemented our approach and applied it to the domains of Zones, Octagon, and Polyhedra. We then compared the performance of the decomposed transformers obtained with our generic method versus the state of the art: the (non-decomposed) PPL for Polyhedra and the much faster ELINA (which uses manual decomposition) for Polyhedra and Octagon. Against ELINA we demonstrate finer partitions and an associated speedup of about 2x on average. Our results indicate that the general construction presented in this work is a viable method for improving the performance of sub-polyhedra domains. It enables designers of abstract domains to benefit from decomposition without re-writing all of their transformers from scratch as required by prior work.
    Type of Medium: Online Resource
    ISSN: 2475-1421
    URL: Article
    DOI: 10.1145/3158143
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2018
    detail.hit.zdb_id: 2924207-1
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 3
    Online Resource
    Online Resource
    Prompting Is Programming: A Query Language for Large Language Models
    Association for Computing Machinery (ACM) ; 2023
    In:  Proceedings of the ACM on Programming Languages Vol. 7, No. PLDI ( 2023-06-06), p. 1946-1969
    Details
    In: Proceedings of the ACM on Programming Languages, Association for Computing Machinery (ACM), Vol. 7, No. PLDI ( 2023-06-06), p. 1946-1969
    Abstract: Large language models have demonstrated outstanding performance on a wide range of tasks such as question answering and code generation. On a high level, given an input, a language model can be used to automatically complete the sequence in a statistically-likely way. Based on this, users prompt these models with language instructions or examples, to implement a variety of downstream tasks. Advanced prompting methods can even imply interaction between the language model, a user, and external tools such as calculators. However, to obtain state-of-the-art performance or adapt language models for specific tasks, complex task- and model-specific programs have to be implemented, which may still require ad-hoc interaction. Based on this, we present the novel idea of Language Model Programming (LMP). LMP generalizes language model prompting from pure text prompts to an intuitive combination of text prompting and scripting. Additionally, LMP allows constraints to be specified over the language model output. This enables easy adaption to many tasks while abstracting language model internals and providing high-level semantics. To enable LMP, we implement LMQL (short for Language Model Query Language), which leverages the constraints and control flow from an LMP prompt to generate an efficient inference procedure that minimizes the number of expensive calls to the underlying language model. We show that LMQL can capture a wide range of state-of-the-art prompting methods in an intuitive way, especially facilitating interactive flows that are challenging to implement with existing high-level APIs. Our evaluation shows that we retain or increase the accuracy on several downstream tasks, while also significantly reducing the required amount of computation or cost in the case of pay-to-use APIs (26-85% cost savings).
    Type of Medium: Online Resource
    ISSN: 2475-1421
    URL: Article
    DOI: 10.1145/3591300
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2023
    detail.hit.zdb_id: 2924207-1
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 4
    Online Resource
    Online Resource
    Efficient data race detection for async-finish parallelism
    Springer Science and Business Media LLC ; 2012
    In:  Formal Methods in System Design Vol. 41, No. 3 ( 2012-12), p. 321-347
    Details
    In: Formal Methods in System Design, Springer Science and Business Media LLC, Vol. 41, No. 3 ( 2012-12), p. 321-347
    Type of Medium: Online Resource
    ISSN: 0925-9856 , 1572-8102
    URL: Article
    DOI: 10.1007/s10703-012-0143-7
    Language: English
    Publisher: Springer Science and Business Media LLC
    Publication Date: 2012
    detail.hit.zdb_id: 1479899-2
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 5
    Online Resource
    Online Resource
    PHALANX : parallel checking of expressive heap assertions
    Association for Computing Machinery (ACM) ; 2010
    In:  ACM SIGPLAN Notices Vol. 45, No. 8 ( 2010-08), p. 41-50
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 45, No. 8 ( 2010-08), p. 41-50
    Abstract: Unrestricted use of heap pointers makes software systems difficult to understand and to debug. To address this challenge, we developed PHALANX -- a practical framework for dynamically checking expressive heap properties such as ownership, sharing and reachability. PHALANX uses novel parallel algorithms to efficiently check a wide range of heap properties utilizing the available cores. PHALANX runtime is implemented on top of IBM's Java production virtual machine. This has enabled us to apply our new techniques to real world software. We checked expressive heap properties in various scenarios and found the runtime support to be valuable for debugging and program understanding. Further, our experimental results on DaCapo and other benchmarks indicate that evaluating heap queries using parallel algorithms can lead to significant performance improvements, often resulting in linear speedups as the number of cores increases. To encourage adoption by programmers, we extended an existing JML compiler to translate expressive JML assertions about the heap into their efficient implementation provided by PHALANX. To debug her program, a programmer can annotate it with expressive heap assertions in JML, that are efficiently checked by PHALANX.
    Type of Medium: Online Resource
    ISSN: 0362-1340 , 1558-1160
    URL: Article
    DOI: 10.1145/1837855.1806658
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2010
    detail.hit.zdb_id: 2079194-X
    detail.hit.zdb_id: 282422-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 6
    Online Resource
    Online Resource
    Deriving linearizable fine-grained concurrent objects
    Association for Computing Machinery (ACM) ; 2008
    In:  ACM SIGPLAN Notices Vol. 43, No. 6 ( 2008-05-30), p. 125-135
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 43, No. 6 ( 2008-05-30), p. 125-135
    Abstract: Practical and efficient algorithms for concurrent data structures are difficult to construct and modify. Algorithms in the literature are often optimized for a specific setting, making it hard to separate the algorithmic insights from implementation details. The goal of this work is to systematically construct algorithms for a concurrent data structure starting from its sequential implementation. Towards that goal, we follow a construction process that combines manual steps corresponding to high-level insights with automatic exploration of implementation details. To assist us in this process, we built a new tool called Paraglider. The tool quickly explores large spaces of algorithms and uses bounded model checking to check linearizability of algorithms. Starting from a sequential implementation and assisted by the tool, we present the steps that we used to derive various highly-concurrent algorithms. Among these algorithms is a new fine-grained set data structure that provides a wait-free contains operation, and uses only the compare-and-swap (CAS) primitive for synchronization.
    Type of Medium: Online Resource
    ISSN: 0362-1340 , 1558-1160
    URL: Article
    DOI: 10.1145/1379022.1375598
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2008
    detail.hit.zdb_id: 2079194-X
    detail.hit.zdb_id: 282422-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 7
    Online Resource
    Online Resource
    Abstraction-guided synthesis of synchronization
    Association for Computing Machinery (ACM) ; 2010
    In:  ACM SIGPLAN Notices Vol. 45, No. 1 ( 2010-01-02), p. 327-338
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 45, No. 1 ( 2010-01-02), p. 327-338
    Abstract: We present a novel framework for automatic inference of efficient synchronization in concurrent programs, a task known to be difficult and error-prone when done manually. Our framework is based on abstract interpretation and can infer synchronization for infinite state programs. Given a program, a specification, and an abstraction, we infer synchronization that avoids all (abstract) interleavings that may violate the specification, but permits as many valid interleavings as possible. Combined with abstraction refinement, our framework can be viewed as a new approach for verification where both the program and the abstraction can be modified on-the-fly during the verification process. The ability to modify the program, and not only the abstraction, allows us to remove program interleavings not only when they are known to be invalid, but also when they cannot be verified using the given abstraction. We implemented a prototype of our approach using numerical abstractions and applied it to verify several interesting programs.
    Type of Medium: Online Resource
    ISSN: 0362-1340 , 1558-1160
    URL: Article
    DOI: 10.1145/1707801.1706338
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2010
    detail.hit.zdb_id: 2079194-X
    detail.hit.zdb_id: 282422-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 8
    Online Resource
    Online Resource
    Making numerical program analysis fast
    Association for Computing Machinery (ACM) ; 2015
    In:  ACM SIGPLAN Notices Vol. 50, No. 6 ( 2015-08-07), p. 303-313
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 50, No. 6 ( 2015-08-07), p. 303-313
    Abstract: Numerical abstract domains are a fundamental component in modern static program analysis and are used in a wide range of scenarios (e.g. computing array bounds, disjointness, etc). However, analysis with these domains can be very expensive, deeply affecting the scalability and practical applicability of the static analysis. Hence, it is critical to ensure that these domains are made highly efficient. In this work, we present a complete approach for optimizing the performance of the Octagon numerical abstract domain, a domain shown to be particularly effective in practice. Our optimization approach is based on two key insights: i) the ability to perform online decomposition of the octagons leading to a massive reduction in operation counts, and ii) leveraging classic performance optimizations from linear algebra such as vectorization, locality of reference, scalar replacement and others, for improving the key bottlenecks of the domain. Applying these ideas, we designed new algorithms for the core Octagon operators with better asymptotic runtime than prior work and combined them with the optimization techniques to achieve high actual performance. We implemented our approach in the Octagon operators exported by the popular APRON C library, thus enabling existing static analyzers using APRON to immediately benefit from our work. To demonstrate the performance benefits of our approach, we evaluated our framework on three published static analyzers showing massive speed-ups for the time spent in Octagon analysis (e.g., up to 146x) as well as significant end-to-end program analysis speed-ups (up to 18.7x). Based on these results, we believe that our framework can serve as a new basis for static analysis with the Octagon numerical domain.
    Type of Medium: Online Resource
    ISSN: 0362-1340 , 1558-1160
    URL: Article
    DOI: 10.1145/2813885.2738000
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2015
    detail.hit.zdb_id: 2079194-X
    detail.hit.zdb_id: 282422-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 9
    Online Resource
    Online Resource
    Dynamic synthesis for relaxed memory models
    Association for Computing Machinery (ACM) ; 2012
    In:  ACM SIGPLAN Notices Vol. 47, No. 6 ( 2012-08-06), p. 429-440
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 47, No. 6 ( 2012-08-06), p. 429-440
    Abstract: Modern architectures implement relaxed memory models which may reorder memory operations or execute them non-atomically. Special instructions called memory fences are provided, allowing control of this behavior. To implement a concurrent algorithm for a modern architecture, the programmer is forced to manually reason about subtle relaxed behaviors and figure out ways to control these behaviors by adding fences to the program. Not only is this process time consuming and error-prone, but it has to be repeated every time the implementation is ported to a different architecture. In this paper, we present the first scalable framework for handling real-world concurrent algorithms running on relaxed architectures. Given a concurrent C program, a safety specification, and a description of the memory model, our framework tests the program on the memory model to expose violations of the specification, and synthesizes a set of necessary ordering constraints that prevent these violations. The ordering constraints are then realized as additional fences in the program. We implemented our approach in a tool called DFence based on LLVM and used it to infer fences in a number of concurrent algorithms. Using DFence, we perform the first in-depth study of the interaction between fences in real-world concurrent C programs, correctness criteria such as sequential consistency and linearizability, and memory models such as TSO and PSO, yielding many interesting observations. We believe that this is the first tool that can handle programs at the scale and complexity of a lock-free memory allocator.
    Type of Medium: Online Resource
    ISSN: 0362-1340 , 1558-1160
    URL: Article
    DOI: 10.1145/2345156.2254115
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2012
    detail.hit.zdb_id: 2079194-X
    detail.hit.zdb_id: 282422-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 10
    Online Resource
    Online Resource
    Testing atomicity of composed concurrent operations
    Association for Computing Machinery (ACM) ; 2011
    In:  ACM SIGPLAN Notices Vol. 46, No. 10 ( 2011-10-18), p. 51-64
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 46, No. 10 ( 2011-10-18), p. 51-64
    Abstract: We address the problem of testing atomicity of composed concurrent operations. Concurrent libraries help programmers exploit parallel hardware by providing scalable concurrent operations with the illusion that each operation is executed atomically. However, client code often needs to compose atomic operations in such a way that the resulting composite operation is also atomic while preserving scalability. We present a novel technique for testing the atomicity of client code composing scalable concurrent operations. The challenge in testing this kind of client code is that a bug may occur very rarely and only on a particular interleaving with a specific thread configuration. Our technique is based on modular testing of client code in the presence of an adversarial environment; we use commutativity specifications to drastically reduce the number of executions explored to detect a bug. We implemented our approach in a tool called COLT, and evaluated its effectiveness on a range of 51 real-world concurrent Java programs. Using COLT, we found 56 atomicity violations in Apache Tomcat, Cassandra, MyFaces Trinidad, and other applications.
    Type of Medium: Online Resource
    ISSN: 0362-1340 , 1558-1160
    URL: Article
    DOI: 10.1145/2076021.2048073
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2011
    detail.hit.zdb_id: 2079194-X
    detail.hit.zdb_id: 282422-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...