|
|
Practical Methods of Automated Verification of Concurrent Programs
Fiedor, Jan ; Arcaini, Paolo (oponent) ; Farchi, Eitan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Nowadays, multi-threaded programs are quite common and so are concurrency errors. Over the years, many techniques were developed to detect such errors, yet software developers still struggle to find the right tools to analyse their programs. The reason is simple, working does not always mean practical. Many tools implementing the detection techniques are hard to use, tailored for a specific kind of programs or synchronisation, or do not scale well to handle large software. For some types of concurrency errors, no tools even exist, yet many software developers encounter such errors in their programs. The main goal of this thesis is to develop new techniques for detecting errors in multi-threaded programs. These techniques should be able to handle complex programs, allow one to detect some of the less studied types of concurrency errors, and support a broad variety of programs.
|
|
|
Slučování úloh s nekolizními požadavky pro systém Beaker
Kovařík, Michal ; Fiedor, Jan (oponent) ; Holík, Lukáš (vedoucí práce)
Obsahem práce je návrh formátu pro zápis parametrů a požadavků jednotlivých úloh určených pro systém Beaker a návrh a implementace programu, který na základě vyloučení možných kolizních požadavků sloučí úlohy definované na vstupu do souboru úloh, jež je možné spouštět společně. Výstupem je formát spustitelný v systému Beaker. Práce popisuje instalaci operačního systému, na kterém definuje kolizní požadavky. V práci je popsán způsob zadávání a spouštění úloh v systému Beaker. V závěru je provedeno testování vytvořeného programu.
|
|
|
Statická analýza v nástroji Meta Infer zaměřená na detekci souběhu nad daty
Svobodová, Lucie ; Fiedor, Jan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Modern software systems often use concurrent programs to improve performance and increase efficiency. However, ensuring the reliability and safety of such systems can be challenging due to the increased potential for bugs, including data races, to arise. In this thesis, we introduce a new static data race detector, DarC, designed for programs written in C using the Pthreads library. The proposed detector is implemented as an analyser plugin in Meta Infer, a static analysis framework with an emphasis on compositional, incremental, and consequently highly-scalable analysis. Our approach involves recording a set of accesses that occur in the analysed program along with information about the set of locks held during these accesses. The tool then identifies pairs of accesses that may lead to data races and reports them to the user. Our tool was successfully evaluated on a set of benchmarking programs as well as on real-life projects, showing its potential for effectively detecting data races in C programs.
|
|
|
Klientská aplikace pro jazykový server Apache Camel
Pospíšil, Filip ; Fiedor, Jan (oponent) ; Vašíček, Ondřej (vedoucí práce)
Předmětem této bakalářské práce je návrh a implementace zásuvného modulu poskytujícího jazykovou podporu pro Apache Camel v integrovaném vývojovém prostředí Apache NetBeans. Cílem práce je umožnit integraci jazykového klienta pro integrované vývojové prostředí Apache NetBeans. Klient ke své funkci využívá již existující jazykový server pro Apache Camel vytvořený společností Red Hat. Práce poskytuje základní úvod k jazykovému protokolu Microsoft Language Protocol, rámci Apache Camel a integrovanému vývojovému prostředí Apache NetBeans. Dále je popsán návrh, implementace a testování vytvořeného jazykového klienta. Výsledkem této práce je zásuvný modul poskytující komplexní jazykovou podporu pro rámec Apache Camel ve vývojovém prostředí Apache NetBeans. Zásuvný modul bude v budoucnu zveřejněn v repozitáři zásuvných modulů Apache NetBeans Plugin Portal.
|
|
|
Unified Access to Requirements in JIRA
Pindur, Daniel ; Vašíček, Ondřej (oponent) ; Fiedor, Jan (vedoucí práce)
The goal of this work is to create an interface for accessing requirements resources stored in Jira Software with the Requirements for Jira (R4J) plugin using an OSLC adaptor for the Requirements Management specification. The adaptor has been split into two to explore the possibility of not needing the R4J plugin - one for the Jira Software (satisfying all requirements of the Requirement Management specification) and one for the R4J plugin (providing additional functionality). Both adaptors have been implemented by utilizing the Eclipse Lyo tooling and the OSLC4J library. The basic overview of the fundamental technologies of OSLC, OSLC Core and Requirement Management specifications, Jira and R4J is provided. The thesis contains a detailed summary of the adaptors' design, implementation, and testing process, as well as an evaluation of the results and used technologies.
|
|
|
Analysis of Software Resource Consumption
Míchal, Ondřej ; Fiedor, Jan (oponent) ; Pavela, Jiří (vedoucí práce)
Software resource consumption is a widely and actively researched area. Of the many resources utilized by software which can be profiled, energy consumption has long been the one resource without many generic, and yet comprehensive profilers. In the age of mobile devices and efficient processing units the need for such profiles is continuously increasing. In this work, we research methods for accurate measurement of energy consumption of software based on them create an open-source profiler and implement a comprehensive visualizer of the profiled data. Using the developed profiler we conduct a number of experiments to showcase its capabilities and demonstrate the usefulness of measuring software energy consumption.
|
|
|
Modeling and Simulation of Incentive Mechanisms in Ethereum
Burianová, Tereza ; Fiedor, Jan (oponent) ; Perešíni, Martin (vedoucí práce)
The topic of this thesis is the Ethereum incentive mechanism, in particular the changes introduced in EIP-1559. The aim of the thesis is to investigate the behaviour and propose any potential improvements in case of discovered flaws. The previously used first price auction mechanism required users to choose the incentive arbitrarily, which led to overpaying and high fee volatility. These problems occurred mainly due to higher network utilization after the popularization of projects such as decentralized finance, NFT collections, and the metaverse. The new incentive mechanism introduced the variable block size, which can adapt to the current network usage. Base fee, a value that indicates the minimum fee needed to include the transaction in the block, is then calculated based on the utilization of the previous block, making the fees more predictable. Several simulation experiments were proposed to investigate the typical behaviour and possible weaknesses of the mechanism. Finally, a possible improvement was found, and future research was proposed. The goals of the thesis were achieved, and the results were presented in the thesis.
|
|
|
Performance Analysis of Programs Based on PIN Framework
Močáry, Peter ; Fiedor, Jan (oponent) ; Pavela, Jiří (vedoucí práce)
The goal of this thesis is to extend the Performance Version System - Perun by implementing a new Tracer engine leveraging PIN instrumentation framework. This extension implements basic Tracer functionality and, in addition to that, a recording of function arguments' values as well as basic block run-times. The additional data, along with the visualizations introduced in this thesis, provide the necessary context that simplifies the detection of performance degradation. Besides the PIN framework, the new Tracer engine implements an analysis of debug information in DWARF format (using the python pyelftools library) to gather details about function arguments before the data collection process. The resulting engine was tested on multiple implementations of sorting algorithms and successfully detected the most time consuming functions along with the information about the effect of its parameter value on the functions complexity. Testing the PIN engine on a larger-scale project revealed that, in comparison to other Tracer engine implementations, the engine performs better or comparably, and produces the correct output.
|
|
|
Efficient Techniques for Program Performance Analysis
Pavela, Jiří ; Fiedor, Jan (oponent) ; Rogalewicz, Adam (vedoucí práce)
In this work, we propose optimization techniques focused on the data collection process of program performance analysis and profiling within the Perun framework. We enhance Perun (and especially its Tracer module) by extending their architecture and implementing novel optimization techniques that allow Perun to scale well even for large projects and test scenarios. In particular, we focus on improving the data collection precision, scaling down the amount of injected instrumentation, limiting the time overhead of the collection and profiling processes, reducing the volume of raw performance data and the size of the resulting profile. To achieve such optimization, we utilized statistical methods, several static and dynamic analysis approaches (as well as their combination) and exploited the advanced features and capabilities of SystemTap and eBPF frameworks. Based on the evaluation performed on two selected projects and numerous experiment cases, we were able to conclude that we successfully achieved significant levels of optimization for nearly all of the identified metrics and criteria.
|
|
|
Využití databáze H2 v JBoss aplikačním serveru
Penčikov, Michal ; Fiedor, Jan (oponent) ; Letko, Zdeněk (vedoucí práce)
JBoss aplikační server (AS) je open source implementace standardu Java EE. Jeho aktuálně používaná databáze pro potřeby testování, HSQL, má některá podstatná omezení, proto existují požadavky na využití jiných databází, použitelných při testování JBoss AS. H2 je relativně nová relační databáze, napsaná čistě v Javě. Tato práce popisuje, jak lze JBoss AS nakonfigurovat, aby místo HSQL databáze používal H2 databázi. Dále uvádí výsledky testů, provedených po této rekonfiguraci a identifikuje problémy, které bude nutno vyřešit, aby JBoss AS mohl používat databázi H2.
|
host ::
RSS.