Skip to main content
Top

2014 | Book

Programming Languages

18th Brazilian Symposium, SBLP 2014, Maceio, Brazil, October 2-3, 2014. Proceedings

Editor: Fernando Magno Quintão Pereira

Publisher: Springer International Publishing

Book Series : Lecture Notes in Computer Science

insite
SEARCH

About this book

This book constitutes the proceedings of the 18th Brazilian Symposium on Programming Languages, SBLP 2014, held in Maceio, Brazil, in October 2014. The 11 full papers were carefully reviewed and selected from 31 submissions. The papers cover topics such as program generation and transformation; programming paradigms and styles; formal semantics and theoretical foundations; program analysis and verification; programming language design and implementation.

Table of Contents

Frontmatter
A Mixed Approach for Building Extensible Parsers
Abstract
For languages whose syntax is fixed, parsers are usually built with a static structure. The implementation of features like macro mechanisms or extensible languages requires the use of parsers that may be dynamically extended. In this work, we discuss a mixed approach for building efficient top-down dynamically extensible parsers. Our view is based on the fact that a large part of the parser code can be statically compiled and only the parts that are dynamic should be interpreted for a more efficient processing. We propose the generation of code for the base parser, in which hooks are included to allow efficient extension of the underlying grammar and activation of a grammar interpreter whenever it is necessary to use an extended syntax. As a proof of concept, we present a prototype implementation of a parser generator using Adaptable Parsing Expression Grammars (APEG) as the underlying method for syntax definition. We show that APEG has features which allow an efficient implementation using the proposed mixed approach.
Leonardo Vieira dos Santos Reis, Vladimir Oliveira Di Iorio, Roberto S. Bigonha
A Security Types Preserving Compiler in Haskell
Abstract
The analysis of information flow has become a popular technique for ensuring the confidentiality of data. An end-to-end confidentiality policy guarantees that private data cannot be inferred by the inspection of public data. A security property that ensures a kind of confidentiality is the noninterference property, which can be enforced by the use of security type systems where types correspond to security levels. In this paper we show the development of a compiler (written in Haskell) between a simple imperative language and semi-structured machine code, which preserves the property of noninterference. The compiler is based on the use of typed abstract syntax (implemented in terms of Haskell GADTs and type-level functions) to encode the security type system of both the source and target language. This makes it possible to use Haskell’s type checker to verify two things: that programs in both languages satisfy the security property, and that the compiler is correct by construction (in the sense that it preserves noninterference).
Cecilia Manzino, Alberto Pardo
Avoiding Code Pitfalls in Aspect-Oriented Programming
Abstract
Aspect-Oriented Programming (AOP) is a maturing technique that requires a good comprehension of which types of mistakes programmers make during the development of applications. Unfortunately, the lack of such knowledge seems to represent one of the reasons for the cautious adoption of AOP in real software development projects. Based on a series of experiments, this paper reports a catalogue of code pitfalls that are likely to lead programmers to make mistakes in AOP. Each experiment required the aspectization (i.e. refactoring) of a crosscutting concern in one object-oriented application. Six rounds of the experiment provided us with the data of 80 aspect-oriented (AO) implementations where three crosscutting concerns were aspectized in three applications. We developed a prototype tool to warn programmers of the code pitfalls during refactoring activities.
Péricles Alves, Eduardo Figueiredo, Fabiano Ferrari
Bounds Check Hoisting for AddressSanitizer
Abstract
The C programming language is not memory safe, that is to say that the semantics of out-of-bounds memory accesses are undefined. There are tools that make certain guarantees about memory safety for C programs. Amongst these are SAFECode and AddressSanitizer. The latter instruments C programs with runtime checks to guarantee that no invalid memory accesses are allowed to execute. As is to be expected, this incurs in a notable performance decrease in instrumented programs. Our work consists in hoisting these checks out of loops in such a way that we maintain AddressSanitizer’s semantics, but, by providing increased locality of access and by increasing the stride of bounds checks, we make said checks notably cheaper. Unlike previous approaches to bounds check hoisting, we use a parametric interval analysis to bound the index ranges used in array accesses. We evaluated our method on a collection of benchmarks from Polybench and from the domain of scientific computing. The optimization recovers 60.6 % of the overhead introduced by AddressSanitizer on average. Since energy performance is a crucial factor on mobile systems, we have also evaluated our proposed solution on embedded systems in this regard. We observed a 31.7 % reduction in energy consumption in programs instrumented with AddressSanitizer.
Simon Moll, Henrique Nazaré, Gustavo Vieira Machado, Raphael Ernani Rodrigues
Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda
Abstract
We present a full certification of merge sort in the language Agda. It features: termination warrant without explicit proof, no proof cost to ensure that the output is sorted, and a succinct proof that the output is a permutation of the input.
Ernesto Copello, Álvaro Tasistro, Bruno Bianchi
Detecting Anomalous Energy Consumption in Android Applications
Abstract
The use of powerful mobile devices, like smartphones, tablets and laptops, is changing the way programmers develop software. While in the past the primary goal to optimize software was the run time optimization, nowadays there is a growing awareness of the need to reduce energy consumption.
This paper presents a technique and a tool to detect anomalous energy consumption in Android applications, and to relate it directly with the source code of the application.
We propose a dynamically calibrated model for energy consumption for the Android ecosystem that supports different devices. The model is used as an API to monitor the application execution: first, we instrument the application source code so that we can relate energy consumption to the application source code; second, we use a statistical approach, based on fault-localization techniques, to localize abnormal energy consumption in the source code.
Marco Couto, Tiago Carção, Jácome Cunha, João Paulo Fernandes, João Saraiva
Effect Capabilities for Haskell
Abstract
Computational effects complicate the tasks of reasoning about and maintaining software, due to the many kinds of interferences that can occur. While different proposals have been formulated to alleviate the fragility and burden of dealing with specific effects, such as state or exceptions, there is no prevalent robust mechanism that addresses the general interference issue. Building upon the idea of capability-based security, we propose effect capabilities as an effective and flexible manner to control monadic effects and their interferences. Capabilities can be selectively shared between modules to establish secure effect-centric coordination. We further refine capabilities with type-based permission lattices to allow fine-grained decomposition of authority. We provide an implementation of effect capabilities in Haskell, using type classes to establish a way to statically share capabilities between modules, as well as to check proper access permissions to effects at compile time. We exemplify how to tame effect interferences using effect capabilities, by treating state and exceptions.
Ismael Figueroa, Nicolas Tabareau, Éric Tanter
Fusion: Abstractions for Multicore/Manycore Heterogenous Parallel Programming Using GPUs
Abstract
Graphic processing units (GPU) have been consolidated as general-purpose computational devices that combine a challenging programming model with an impressive acceleration of HPC programs whose total execution time are dominated by performance-critical small sections of code. However, there is still a lack of high-level programming language abstractions for better specifying heterogenous parallel computations using these devices. This paper proposes Fusion, an extension of Java that introduces new abstractions for heterogenous multicore-GPU programming, taking advantage of new features introduced by the NVIDIA’s Kepler architecture, such as Hyper-Q and Dynamic Parallelism.
Anderson Boettge Pinheiro, Francisco Heron de Carvalho Junior, Neemias Gabriel Pena Batista Arruda, Tiago Carneiro
Real-World Loops Are Easy to Predict
Abstract
The Trip Count of a loop determines how many iterations this loop performs. Several compiler optimizations yield greater benefits for large trip counts, and are either innocuous or detrimental for small ones. However, predicting exactly the trip count of a loop is an undecidable problem in general. Thus, such problem is usually approached through heuristics, which tend to be computationally expensive. In this paper we argue that in most cases there is no need to resort to expensive methods and that in many cases the trip count prediction does not need to be sound. In that sense, we propose a lightweight trip count prediction heuristic. Our method identifies the pattern on which the induction variables of each loop are updated between two iterations and generate symbolic expressions that represent the trip counts of the loops. Such expressions can be evaluated at runtime with O(1) complexity and allow blocks of code to be conditionally executed, depending on the expected trip count. We argue that such technique is useful for speculative optimizations, very common in the world of just-in-time compilers. For instance, if we predict that a loop will iterate for a long time, we can perform more aggressive JIT optimizations. Furthermore, we show that despite the simplicity of our technique, we have accurately predicted nearly 90% of all the interval loops found in millions of lines of C code. The interval loops represent approximately 67% of the total number of loops of the programs.
Raphael Ernani Rodrigues
A Hybrid Framework to Accelerate Adaptive Compilation Systems
Abstract
Virtual execution is a method to reduce the prohibitive overhead of the execution step on adaptive compilation systems. Nevertheless it may fail to identify the best compiler optimizations set, reducing the speedup that could be achieved by the adaptive compilation system. We discuss the shortcomings of the virtual execution method and propose a hybrid mechanism, which leverages the virtual execution method to select a few optimizations sets before performing the execution step to select the best set of optimizations.
Gabriel Krisman Bertazi, Anderson Faustino da Silva, Edson Borin
Transactional Boosting for Haskell
Abstract
Transactional boosting is a methodology used to transform highly concurrent linearizable objects into highly concurrent transactional objects. In this paper we describe a STM Haskell extension that allows programmers to write boosted versions of highly concurrent abstract data types. Although the technique can only be applied to abstract types that have certain properties, when used correctly, we obtain transactional versions of existing types that are much faster than if they were implemented with pure STM Haskell.
André Rauber Du Bois, Maurício Lima Pilla, Rodrigo Duarte
Backmatter
Metadata
Title
Programming Languages
Editor
Fernando Magno Quintão Pereira
Copyright Year
2014
Publisher
Springer International Publishing
Electronic ISBN
978-3-319-11863-5
Print ISBN
978-3-319-11862-8
DOI
https://doi.org/10.1007/978-3-319-11863-5

Premium Partner