Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Publications

Publications by João Bispo

2021

Formal verification of Matrix based MATLAB models using interactive theorem proving

Authors
Gauhar, A; Rashid, A; Hasan, O; Bispo, J; Cardoso, JMP;

Publication
PEERJ COMPUTER SCIENCE

Abstract
MATLAB is a software based analysis environment that supports a high-level programing language and is widely used to model and analyze systems in various domains of engineering and sciences. Traditionally, the analysis of MATLAB models is done using simulation and debugging/testing frameworks. These methods provide limited coverage due to their inherent incompleteness. Formal verification can overcome these limitations, but developing the formal models of the underlying MATLAB models is a very challenging and time-consuming task, especially in the case of higher-order-logic models. To facilitate this process, we present a library of higher-order-logic functions corresponding to the commonly used matrix functions of MATLAB as well as a translator that allows automatic conversion of MATLAB models to higher-order logic. The formal models can then be formally verified in an interactive theorem prover. For illustrating the usefulness of the proposed library and approach, we present the formal analysis of a Finite Impulse Response (FIR) filter, which is quite commonly used in digital signal processing applications, within the sound core of the HOL Light theorem prover.

2021

A Binary Translation Framework for Automated Hardware Generation

Authors
Paulino, N; Bispo, J; Ferreira, JC; Cardoso, JMP;

Publication
IEEE MICRO

Abstract
As applications move to the edge, efficiency in computing power and power/energy consumption is required. Heterogeneous computing promises to meet these requirements through application-specific hardware accelerators. Runtime adaptivity might be of paramount importance to realize the potential of hardware specialization, but further study is required on workload retargeting and offloading to reconfigurable hardware. This article presents our framework for the exploration of both offloading and hardware generation techniques. The framework is currently able to process instruction sequences from MicroBlaze, ARMv8, and riscv32imaf binaries, and to represent them as Control and Dataflow Graphs for transformation to implementations of hardware modules. We illustrate the framework's capabilities for identifying binary sequences for hardware translation with a set of 13 benchmarks.

2021

Multi-language static code analysis on the LARA framework

Authors
Teixeira, G; Bispo, J; Correia, FF;

Publication
SOAP@PLDI 2021: Proceedings of the 10th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, Virtual Event, Canada, 22 June, 2021

Abstract
We propose a mechanism to raise the abstraction level of source-code analysis and robustly support multiple languages. Built on top of the LARA framework, it allows sharing language specifications between LARA source-to-source compilers, and enables the mapping of a virtual AST over the nodes of ASTs provided by different, unrelated parsers. We use this approach to create a language specification for Object-Oriented (OO) languages and add support for three different LARA compilers. We evaluate it by implementing a library of 18 software metrics using this language specification and apply the metrics to source code in four programming languages (C, C++, Java, and JavaScript). We compare the results with other tools to evaluate the approach.

2020

Clava: C/C plus plus source-to-source compilation using LARA

Authors
Bispo, J; Cardoso, JMP;

Publication
SOFTWAREX

Abstract
This article presents Clava, a Clang-based source-to-source compiler, that accepts scripts written in LARA, a JavaScript-based DSL with special constructs for code queries, analysis and transformations. Clava improves Clang's source-to-source capabilities by providing a more convenient and flexible way to analyze, transform and generate C/C++ code, and provides support for building strategies that capture run-time behavior. We present the Clava framework, its main capabilities, and how it can been used. Furthermore, we show that Clava is sufficiently robust to analyze, instrument and test a set of large C/C++ application codes, such as GCC. (C) 2020 The Authors. Published by Elsevier B.V.

2020

Compilation of MATLAB computations to CPU/GPU via C/OpenCL generation

Authors
Reis, L; Bispo, J; Cardoso, JMP;

Publication
CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE

Abstract
In order to take advantage of the processing power of current computing platforms, programmers typically need to develop software versions for different target devices. This task is time-consuming and requires significant programming and computer architecture expertise. A possible and more convenient alternative is to start with a single high-level description of a program with minimum implementation details, and generate custom implementations according to the target platform. In this paper, we use MATLAB as a high-level programming language and propose a compiler that targets CPU/GPU computing platforms by generating customized implementations in C and OpenCL. We propose a number of compiler techniques to automatically generate efficient C and OpenCL code from MATLAB programs. One of such compiler techniques relies on heuristics to decide when and how to use Shared Virtual Memory (SVM). The experimental results show that our approach is able to generate code that provides significant speedups (eg, geometric mean speedup of 11x for a set of simple benchmarks) using a discrete GPU over equivalent sequential C code executing on a CPU. With more complex benchmarks, for which only some code regions can be parallelized, and are thus offloaded, the generated code achieved speedups of up to 2.2x. We also show the impact of using SVM, specifically fine-grained buffers, and the results show that the compiler is able to achieve significant speedups, both over the versions without SVM and with naive aggressive SVM use, across three CPU/GPU platforms.

2021

On the Performance Effect of Loop Trace Window Size on Scheduling for Configurable Coarse Grain Loop Accelerators

Authors
Santos, T; Paulino, N; Bispo, J; Cardoso, JMP; Ferreira, JC;

Publication
2021 INTERNATIONAL CONFERENCE ON FIELD-PROGRAMMABLE TECHNOLOGY (ICFPT)

Abstract
By using Dynamic Binary Translation, instruction traces from pre-compiled applications can be offloaded, at runtime, to FPGA-based accelerators, such as Coarse-Grained Loop Accelerators, in a transparent way. However, scheduling onto coarse-grain accelerators is challenging, with two of current known issues being the density of computations that can be mapped, and the effects of memory accesses on performance. Using an in-house framework for analysis of instruction traces, we explore the effect of different window sizes when applying list scheduling, to map the window operations to a coarse-grain loop accelerator model that has been previously experimentally validated. For all window sizes, we vary the number of ALUs and memory ports available in the model, and comment how these parameters affect the resulting latency. For a set of benchmarks taken from the PolyBench suite, compiled for the 32-bit MicroBlaze softcore, we have achieved an average iteration speedup of 5.10x for a basic block repeated 5 times and scheduled with 8 ALUs and memory ports, and an average speedup of 5.46x when not considering resource constraints. We also identify which benchmarks contribute to the difference between these two speedups, and breakdown their limiting factors. Finally, we reflect on the impact memory dependencies have on scheduling.

  • 6
  • 12