Result page:
1
2
3
4
5
6
7
1
Typed self-evaluation via intensional type functions
January 2017
POPL 2017: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
Publisher: ACM
Bibliometrics:
Citation Count: 0
Downloads (6 Weeks): 14, Downloads (12 Months): 130, Downloads (Overall): 130
Full text available:
PDF
Many popular languages have a self-interpreter, that is, an interpreter for the language written in itself. So far, work on polymorphically-typed self-interpreters has concentrated on self-recognizers that merely recover a program from its representation. A larger and until now unsolved challenge is to implement a polymorphically-typed self-evaluator that evaluates the ...
Keywords:
Lambda Calculus, Meta Programming, Type Equality, Self Evaluation, Self Interpretation, Self Representation
Also published in:
May 2017
ACM SIGPLAN Notices - POPL '17: Volume 52 Issue 1, January 2017
2
Breaking through the normalization barrier: a self-interpreter for f-omega
January 2016
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Publisher: ACM
Bibliometrics:
Citation Count: 1
Downloads (6 Weeks): 5, Downloads (12 Months): 103, Downloads (Overall): 204
Full text available:
PDF
According to conventional wisdom, a self-interpreter for a strongly normalizing lambda-calculus is impossible. We call this the normalization barrier. The normalization barrier stems from a theorem in computability theory that says that a total universal function for the total computable functions is impossible. In this paper we break through the ...
Keywords:
Lambda Calculus, Meta Programming, Self Interpretation, Self Representation
Also published in:
April 2016
ACM SIGPLAN Notices - POPL '16: Volume 51 Issue 1, January 2016
3
Declarative fence insertion
October 2015
OOPSLA 2015: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
Publisher: ACM
Bibliometrics:
Citation Count: 0
Downloads (6 Weeks): 5, Downloads (12 Months): 24, Downloads (Overall): 61
Full text available:
PDF
Previous work has shown how to insert fences that enforce sequential consistency. However, for many concurrent algorithms, sequential consistency is unnecessarily strong and can lead to high execution overhead. The reason is that, often, correctness relies on the execution order of a few specific pairs of instructions. Algorithm designers can ...
Keywords:
Compilers, Static Analysis, Weak Memory Models, Concurrency
Also published in:
December 2015
ACM SIGPLAN Notices - OOPSLA '15: Volume 50 Issue 10, October 2015
4
Self-Representation in Girard's System U
January 2015
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Publisher: ACM
Bibliometrics:
Citation Count: 3
Downloads (6 Weeks): 5, Downloads (12 Months): 31, Downloads (Overall): 171
Full text available:
PDF
In 1991, Pfenning and Lee studied whether System F could support a typed self-interpreter. They concluded that typed self-representation for System F "seems to be impossible", but were able to represent System F in F ω . Further, they found that the representation of F ω requires kind polymorphism, which ...
Keywords:
self representation, theory, lambda calculus, languages, types
Also published in:
May 2015
ACM SIGPLAN Notices - POPL '15: Volume 50 Issue 1, January 2015
5
Sherlock: scalable deadlock detection for concurrent programs
November 2014
FSE 2014: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering
Publisher: ACM
Bibliometrics:
Citation Count: 7
Downloads (6 Weeks): 7, Downloads (12 Months): 85, Downloads (Overall): 256
Full text available:
PDF
We present a new technique to find real deadlocks in concurrent programs that use locks. For 4.5 million lines of Java, our technique found almost twice as many real deadlocks as four previous techniques combined. Among those, 33 deadlocks happened after more than one million computation steps, including 27 new ...
Keywords:
deadlocks, Concurrency
6
July 2014
Proceedings of the 16th International Conference on Computer Aided Verification - Volume 8559
Publisher: Springer-Verlag New York, Inc.
Mainstream programming languages offer libraries of concurrent data structures. Each method call on a concurrent data structure appears to take effect atomically. However, clients of such data structures often require stronger guarantees. For instance, a histogram class that is implemented using a concurrent map may require a method to atomically ...
7
Race directed scheduling of concurrent programs
February 2014
PPoPP '14: Proceedings of the 19th ACM SIGPLAN symposium on Principles and practice of parallel programming
Publisher: ACM
Bibliometrics:
Citation Count: 8
Downloads (6 Weeks): 9, Downloads (12 Months): 45, Downloads (Overall): 226
Full text available:
PDF
Detection of data races in Java programs remains a difficult problem. The best static techniques produce many false positives, and also the best dynamic techniques leave room for improvement. We present a new technique called race directed scheduling that for a given race candidate searches for an input and a ...
Keywords:
concurrency, race detection
Also published in:
November 2014
ACM SIGPLAN Notices - PPoPP '14: Volume 49 Issue 8, August 2014
8
Proving Non-opacity
October 2013
DISC 2013: Proceedings of the 27th International Symposium on Distributed Computing - Volume 8205
Publisher: Springer-Verlag New York, Inc.
Guerraoui and Kapalka defined opacity as a safety criterion for transactional memory algorithms in 2008. Researchers have shown how to prove opacity, while little is known about pitfalls that can lead to non-opacity. In this paper, we identify two problems that lead to non-opacity, we present automatic tool support for ...
9
Testing versus Static Analysis of Maximum Stack Size
July 2013
COMPSAC '13: Proceedings of the 2013 IEEE 37th Annual Computer Software and Applications Conference
Publisher: IEEE Computer Society
For event-driven software on resource-constrained devices, estimates of the maximum stack size can be of paramount importance. For example, a poor estimate led to software failure and closure of a German railway station in 1995. Static analysis may produce a safe estimate but how good is it? In this paper ...
Keywords:
Testing, static analysis, maximum stack size
10
A decoupled local memory allocator
January 2013
ACM Transactions on Architecture and Code Optimization (TACO) - Special Issue on High-Performance Embedded Architectures and Compilers: Volume 9 Issue 4, January 2013
Publisher: ACM
Bibliometrics:
Citation Count: 1
Downloads (6 Weeks): 1, Downloads (12 Months): 16, Downloads (Overall): 276
Full text available:
PDF
Compilers use software-controlled local memories to provide fast, predictable, and power-efficient access to critical data. We show that the local memory allocation for straight-line, or linearized programs is equivalent to a weighted interval-graph coloring problem. This problem is new when allowing a color interval to “wrap around,” and we call ...
Keywords:
memory allocation, Local memory, compiler, scratchpad memory
11
Efficient may happen in parallel analysis for async-finish parallelism
September 2012
SAS'12: Proceedings of the 19th international conference on Static Analysis
Publisher: Springer-Verlag
For concurrent and parallel languages, the may-happen-in-parallel (MHP) decision problem asks, given two actions in the program, if there is an execution in which they can execute in parallel. Closely related, the MHP computation problem asks, given a program, which pairs of statements may happen in parallel. MHP analysis is ...
12
Featherweight X10: a core calculus for async-finish parallelism
June 2012
FTfJP '12: Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs
Publisher: ACM
We present a core calculus with two of X10's key constructs for parallelism, namely async and finish. Our calculus forms a convenient basis for type systems and static analyses for languages with async-finish parallelism. For example, we present a type system for context-sensitive may-happen-in-parallel analysis, along with experimental results of ...
Keywords:
operational semantics, parallelism, static analysis
13
Overloading is NP-Complete
January 2012
Logic and Program Semantics: essays dedicated to Dexter Kozen on the occasion of his 60th birthday
Publisher: Springer-Verlag
We show that overloading is NP-complete. This solves exercise 6.25 in the 1986 version of the Dragon book.
14
Typed self-interpretation by pattern matching
September 2011
ACM SIGPLAN Notices - ICFP '11: Volume 46 Issue 9, September 2011
Publisher: ACM
Bibliometrics:
Citation Count: 6
Downloads (6 Weeks): 3, Downloads (12 Months): 13, Downloads (Overall): 325
Full text available:
PDF
Self-interpreters can be roughly divided into two sorts: self-recognisers that recover the input program from a canonical representation, and self-enactors that execute the input program. Major progress for statically-typed languages was achieved in 2009 by Rendel, Ostermann, and Hofer who presented the first typed self-recogniser that allows representations of different ...
Keywords:
pattern matching, self-interpretation
Also published in:
September 2011
ICFP '11: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming
15
From textual use cases to service component models
May 2011
PESOS '11: Proceedings of the 3rd International Workshop on Principles of Engineering Service-Oriented Systems
Publisher: ACM
Bibliometrics:
Citation Count: 0
Downloads (6 Weeks): 3, Downloads (12 Months): 13, Downloads (Overall): 152
Full text available:
PDF
There is a gap between system requirements described with natural language and system design models described with formal language. In this paper, we present a framework for automatically mapping textual use cases to service component models from a model-based point of view. The generated models capture service component signatures and ...
Keywords:
system requirement, model transformation, natural language processing, textual use case, service component model
16
Communicating memory transactions
February 2011
PPoPP '11: Proceedings of the 16th ACM symposium on Principles and practice of parallel programming
Publisher: ACM
Bibliometrics:
Citation Count: 11
Downloads (6 Weeks): 5, Downloads (12 Months): 15, Downloads (Overall): 252
Full text available:
PDF
Many concurrent programming models enable both transactional memory and message passing. For such models, researchers have built increasingly efficient implementations and defined reasonable correctness criteria, while it remains an open problem to obtain the best of both worlds. We present a programming model that is the first to have opaque ...
Keywords:
transactional memory, actor
Also published in:
September 2011
ACM SIGPLAN Notices - PPoPP '11: Volume 46 Issue 8, August 2011
17
The essence of compiling with traces
January 2011
ACM SIGPLAN Notices - POPL '11: Volume 46 Issue 1, January 2011
Publisher: ACM
Bibliometrics:
Citation Count: 12
Downloads (6 Weeks): 10, Downloads (12 Months): 38, Downloads (Overall): 465
Full text available:
PDF
The technique of trace-based just-in-time compilation was introduced by Bala et al. and was further developed by Gal et al. It currently enjoys success in Mozilla Firefox's JavaScript engine. A trace-based JIT compiler leverages run-time profiling to optimize frequently-executed paths while enabling the optimized code to ``bail out'' to the ...
Keywords:
bisimulation, compiler correctness, just-in-time compilation
Also published in:
January 2011
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
18
From OO to FPGA: fitting round objects into square hardware?
October 2010
OOPSLA '10: Proceedings of the ACM international conference on Object oriented programming systems languages and applications
Publisher: ACM
Bibliometrics:
Citation Count: 1
Downloads (6 Weeks): 5, Downloads (12 Months): 26, Downloads (Overall): 305
Full text available:
PDF
Consumer electronics today such as cell phones often have one or more low-power FPGAs to assist with energyintensive operations in order to reduce overall energy consumption and increase battery life. However, current techniques for programming FPGAs require people to be specially trained to do so. Ideally, software engineers can more ...
Keywords:
objects, FPGAs
Also published in:
October 2010
ACM SIGPLAN Notices - OOPSLA '10: Volume 45 Issue 10, October 2010
19
Concurrent Collections
Zoran Budimlić,
Michael Burke,
Vincent Cavé,
Kathleen Knobe,
Geoff Lowney,
Ryan Newton,
Jens Palsberg,
David Peixotto,
Vivek Sarkar,
Frank Schlimbach,
Sağnak Taşırlar
August 2010
Scientific Programming - Exploring Languages for Expressing Medium to Massive On-Chip Parallelism: Volume 18 Issue 3-4, August 2010
Publisher: IOS Press
We introduce the Concurrent Collections (CnC) programming model. CnC supports flexible combinations of task and data parallelism while retaining determinism. CnC is implicitly parallel, with the user providing high-level operations along with semantic ordering constraints that together form a CnC graph. We formally describe the execution semantics of CnC and ...
Keywords:
Concurrent Collections (CnC), parallel programming, programming model
20
Punctual coalescing
March 2010
CC'10/ETAPS'10: Proceedings of the 19th joint European conference on Theory and Practice of Software, international conference on Compiler Construction
Publisher: Springer-Verlag
Compilers use register coalescing to avoid generating code for copy instructions. For architectures with register aliasing such as x86, Smith, Ramsey, and Holloway (2004) presented a polynomial-time approach, while Scholz and Eckstein (2002) presented an optimal, exponential-time approach together with a near-optimal, quadratic-time heuristic. Both methods scale poorly after aggressive ...
Author only
