|
|
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.
|
|
|
SIMD code generator
Tuček, Karel ; Bednárek, David (vedoucí práce) ; Arcaini, Paolo (oponent)
Title: SIMD code generator Author: Karel Tuček Department: Department of Software Engineering Supervisor: RNDr. David Bednárek, Ph.D., Department of Software Engineering Abstract: The center of our interest is a problem of pipelined realisation of a special case of data processing networks. These realisations are supposed to realise some computations on series of independent data sets while utilizing SIMD instructions. The aim of this paper is to theoretically investigate the possibilities and the problems of employment of control flow in these networks and also to implement a general framework suitable for generation of these realisations. The main idea is utilisation of an algorithm crawling over partitions of a network factorised with respect to its control flow. Our idea is that SIMD parallelism should take place on the same instruction realised across multiple data sets. We illustrate the problems relevant to employment of branching and loops in these networks. We especially discuss a problem of data ordering and also provide relevant proofs. In the analytical part, we show implementation of a general framework which we believe to be suitable for processing of these networks. We also provide examples utilising Intel's SIMD Streaming Extensions. Keywords: Processing networks SIMD Parallelism iii
|
|
|
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.
|
|
|
SIMD code generator
Tuček, Karel ; Bednárek, David (vedoucí práce) ; Arcaini, Paolo (oponent)
Title: SIMD code generator Author: Karel Tuček Department: Department of Software Engineering Supervisor: RNDr. David Bednárek, Ph.D., Department of Software Engineering Abstract: The center of our interest is a problem of pipelined realisation of a special case of data processing networks. These realisations are supposed to realise some computations on series of independent data sets while utilizing SIMD instructions. The aim of this paper is to theoretically investigate the possibilities and the problems of employment of control flow in these networks and also to implement a general framework suitable for generation of these realisations. The main idea is utilisation of an algorithm crawling over partitions of a network factorised with respect to its control flow. Our idea is that SIMD parallelism should take place on the same instruction realised across multiple data sets. We illustrate the problems relevant to employment of branching and loops in these networks. We especially discuss a problem of data ordering and also provide relevant proofs. In the analytical part, we show implementation of a general framework which we believe to be suitable for processing of these networks. We also provide examples utilising Intel's SIMD Streaming Extensions. Keywords: Processing networks SIMD Parallelism iii
|
|
|
Optimization of DEECo gossip-based communication
Kováč, Ondrej ; Bureš, Tomáš (vedoucí práce) ; Arcaini, Paolo (oponent)
Rozšiřování velkého počtu bezdrátových zařízení dalo podnět ke vzniku komponentového modelu DEECo určeného pro aplikace, jejichž neoddělitelnou součástí je mobilita a dynamická kompozice s architekturou vytvářenou za běhu. Velkou výzvou při realizaci takového systému je návrh komunikačního systému založeném na gossip protokolu. Takové řešení je zvlášť vhodné pro sítě typu MANET a jeho účelem je zvýšení spolehlivosti. V této práci jsme navrhli optimalizaci protokolu s využitím vlastností sítě s vlastní infrastrukturou. Zachovali jsme při tom gossip způsob komunikace bez zavedení centralizovaného prvku. Navrhované zlepšení spočívá ve vytvoření komunikačních skupin zformovaných na úrovni návrhu. Experimenty ukázaly podstatný pokles počtu odeslaných zpráv a celkově snížený čas doručení. Problematiku časování jsme pak zvlášť zpracovali pro MANET sítě a implementovali jsme mechanizmus pullování, který významně snížil latenci. Část této práce je věnována formální specifikaci sémantiky za účelem přesného zdůvodnění vlastností systému, čímž jsme také položili základ pro další rozšíření protokolu a budoucí výzkum v oblasti distribuovaných systémů. Powered by TCPDF (www.tcpdf.org)
|
|
|
Meta-Adaptation Strategies for Adaptation in Cyber-Physical Systems
Huječek, Adam ; Bureš, Tomáš (vedoucí práce) ; Arcaini, Paolo (oponent)
Při návrhu komplexních cyber-physical systémů je často nemožné dopředu předvídat všechny potencionální situace a připravit odpovídající taktiky pro adaptaci na změny v dynamickém prostředí, což velmi škodí robustnosti a spolehlivosti těchto systémů. Ze situací mimo očekávanou "obálku adaptability" mohou povstat všemožné problémy, od poruchy jedné komponenty až po selhání celého systému. Samoadaptační přístupy jsou typicky omezeny na volbu taktiky z pevně dané množiny taktik. Meta-adaptační strategie posouvají hranice adaptability vlastní systému vytvářením nových taktik za běhu. Tato práce rozvíjí a implementuje vybrané meta-adaptace pro IRM-SA v jDEECo a vyhodnocuje jejich účinnost na experimentálním scénáři založeném na případové studii o koordinaci hasičů. Powered by TCPDF (www.tcpdf.org)
|
host ::
RSS.