|
|
Static Analysis Using Facebook Infer to Find Atomicity Violations
Harmim, Dominik ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
The goal of this thesis is to propose a static analyser that detects atomicity violations. The proposed analyser Atomer is implemented as a module of Facebook Infer, which is an open-source and extendable static analysis framework that promotes efficient modular and incremental analysis. The analyser works on the level of sequences of function calls. The proposed solution is based on the assumption that sequences executed atomically once should probably be executed always atomically. The implemented analyser has been successfully verified and evaluated on both smaller programs created for testing purposes as well as publicly available benchmarks derived from real-life low-level programs.
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Nástroj Atomer je statický analyzátor založený na myšlence, že pokud jsou některé sekvence funkcí vícevláknového programu prováděny v některých bězích pod zámky, je pravděpodobně zamýšleno, že mají být vždy provedeny atomicky. Analyzátor Atomer se tudíž snaží takové sekvence hledat a poté zjišťovat, pro které z nich může být v některých jiných bězích programu porušena atomicita. Autor této diplomové práce ve své bakalářské práci navrhl a implementoval první verzi nástroje Atomer jako zásuvný modul aplikačního rámce Facebook Infer. V této diplomové práci je navržena nová a výrazně vylepšená verze analyzátoru Atomer. Cílem vylepšení je zvýšení jak škálovatelnosti, tak přesnosti. Kromě toho byla přidána podpora pro několik původně nepodporovaných programovacích vlastností (včetně např. možnosti analyzovat programy napsané v jazycích C++ a Java nebo podpory pro reentrantní zámky nebo stráže zámků, tzv. "lock guards"). Prostřednictvím řady experimentů (včetně experimentů s reálnými programy a reálnými chybami) se ukázalo, že nová verze nástroje Atomer je skutečně mnohem obecnější, přesnější a lépe škáluje.
|
|
|
Roots of Moravian Urban Structure
Mohelník, Ladislav ; Löw, Jiří (referee) ; Prokeš, Oldřich (referee) ; Hrabec, Josef (referee) ; Koutný, Jan (advisor)
The thesis has been written on the basis of main architectural concepts and their application in real life within a historical context investigation. Main architectural concepts are represented in a harmony of architectural composition that deals with relations among form, structure and space in the unique art work. Genius loci play very important role in the architectural creation - it represents a special and extra-ordinary urban locality and its architectural value in the historical, geographical and cultural context. The origin of Ostravice village within the historical frame concept of Moravia domain is the topic of this thesis. Other historical documents gave information about Bruneswerde as the Brno Castle. That means Brno Castle had to be founded not in Brno (as it has been consid-ered for many years) but it was located in Beskydy at Ostravice. The sacred city – Civitas Dei had been located in Bruneswerde region in early ages as the centre of European culture, education and spiritual life. Civitas Dei – divine Jerusalem in the transcription of St. Augustine's book De civitate Dei – is not only glorification of God and religious fantasy. It is also one of significant clues for recognition of historical architecture. The depiction of unknown settlement from the book of unde-fined origin is a superb testimony about extinct architectural works. They are legible from cadastral maps. Brno Castle - residence of nobility and power served shelter to St. Vojtěch, St. Prokop, St. Václav and St. Ludmila as it is obvious for the mentioned picture. Three major temples, three com-position axes symbolized by three towers on coins are in analogical relation to Brno triangle of four saints - the Saint family of Brno temples. Powerful ambitions of Brno City principals and clergy are inscribed into the urban structure in the way of composition relations which are legible to them who devoted themselves to the mystery of harmony. The absence of historical continuity affects personal attitudes and also identity of the whole community. The architecture truly reflects the past state of polis and it is eloquent even after its death. The architectural composition relations influence the natural environment for long time, longer than the architectural work existence. The geometric order of Renaissance Brno existence has not been in attention of architects so far. The features were discovered in characteristic paintings by Albrecht Durer. They are evidently secret works of the genius. A meaningful collaborator and follower in the extensive project was also his friend Jan Čert from Brno and lately from Vienna. His noble genealogy played a significant role in history of Silesia and Moravia for centuries. It is tendency to consider him as Austrian or even German architect. It is because of the fact that the genealogy tree of his noble family had roots in Moravia. It is supposed that Durer with Jan Čert´s support created the extraordinarily monumental architectural and urban works in Brno. A remarkable consensus in the urban composition of two squares and transition of traditional urban structure of Ostravice Civitas Dei into the modern Brno is also confirmed due to the identification of noble creators and owners, who were at the foundation, transformation and extinction of elements of the Moravian urban structure.
|
|
|
Pokročilá statická analýza výkonnosti v nástroji Meta Infer
Pavela, Ondřej ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Statický analyzátor složitosti Looper slouží pro odvozování přesných horních mezí ceny vykonání programů. Jako teoretický základ byl využit dříve existující nástroj Loopus a jeho abstraktní programový model využívající tzv. difference constraints (nerovnosti typu + ), které umožňují přirozeným způsobem modelovat typické modifikace počítadel cyklů = + + a = + 0. Looper byl původně navržen a implementován v rámci autorovy bakalářské práce jako zásuvný modul aplikačního rámce Meta Infer. Výsledný nástroj nicméně nenaplnil očekávání při pokusech o jeho nasazení na reálné programy. Tato diplomová práce představuje návrh nové verze, která si dává za cíl odstranit hlavní limitace původního nástroje Looper, zejména díky nově podporované in- terprocedurální analýze. Dále byla implementována řada rozšíření, které cílily na zvýšení přesnosti intraprocedurální analýzy, jako např. nový abstrakční algoritmus, podpora pro složené podmínky v hlavičkách smyček a další. Kromě toho bylo také výrazně vylepšeno logování, hlášení chyb a sběr výsledků analýzy. Na závěr byla skrze skrze rozsáhlé exper- imenty demonstrována schopnost nové verze nástroje Looper analyzovat reálný kód obec- nějším, škálovatelnějším a přesnějším způsobem.
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Nástroj Atomer je statický analyzátor založený na myšlence, že pokud jsou některé sekvence funkcí vícevláknového programu prováděny v některých bězích pod zámky, je pravděpodobně zamýšleno, že mají být vždy provedeny atomicky. Analyzátor Atomer se tudíž snaží takové sekvence hledat a poté zjišťovat, pro které z nich může být v některých jiných bězích programu porušena atomicita. Autor této diplomové práce ve své bakalářské práci navrhl a implementoval první verzi nástroje Atomer jako zásuvný modul aplikačního rámce Facebook Infer. V této diplomové práci je navržena nová a výrazně vylepšená verze analyzátoru Atomer. Cílem vylepšení je zvýšení jak škálovatelnosti, tak přesnosti. Kromě toho byla přidána podpora pro několik původně nepodporovaných programovacích vlastností (včetně např. možnosti analyzovat programy napsané v jazycích C++ a Java nebo podpory pro reentrantní zámky nebo stráže zámků, tzv. "lock guards"). Prostřednictvím řady experimentů (včetně experimentů s reálnými programy a reálnými chybami) se ukázalo, že nová verze nástroje Atomer je skutečně mnohem obecnější, přesnější a lépe škáluje.
|
|
|
Static Analysis Using Facebook Infer to Find Atomicity Violations
Harmim, Dominik ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
The goal of this thesis is to propose a static analyser that detects atomicity violations. The proposed analyser Atomer is implemented as a module of Facebook Infer, which is an open-source and extendable static analysis framework that promotes efficient modular and incremental analysis. The analyser works on the level of sequences of function calls. The proposed solution is based on the assumption that sequences executed atomically once should probably be executed always atomically. The implemented analyser has been successfully verified and evaluated on both smaller programs created for testing purposes as well as publicly available benchmarks derived from real-life low-level programs.
|
|
|
Bedřich Kocek and czech press photography
Sýkorová, Tereza ; Láb, Filip (advisor) ; Géla, František (referee)
The master thesis Bedřich Kocek and Czech Press Photography is concerned with the life and work of Bedřich Kocek - Czech photojournalist who worked in the renowned journal Svět v obrazech (translated as World in Pictures) for over thirty years. The theoretical part specifies the genre of journalistic photography and its development from the turn of the 19th and 20th centuries to the 1980s. Furthermore, the development of the journal Svět v obrazech serves as an example for outlining the media and political context in Czechoslovakia since the end of World War II, when the periodical was established, until the 1980s, when Bedřich Kocek left the profession of a photojournalist. An especially valuable and vital part of the thesis is a chapter about the life of Bedřich Kocek, which has not been previously researched and described in detail. That section is based on personal interviews with the photographer using the oral history method. Moreover, the thesis explores the photographic work of Bedřich Kocek through the use of compositional analysis as well as the characteristic features of his pictures, which were part of the reports produced for Svět v obrazech.
|
|
|
Roots of Moravian Urban Structure
Mohelník, Ladislav ; Löw, Jiří (referee) ; Prokeš, Oldřich (referee) ; Hrabec, Josef (referee) ; Koutný, Jan (advisor)
The thesis has been written on the basis of main architectural concepts and their application in real life within a historical context investigation. Main architectural concepts are represented in a harmony of architectural composition that deals with relations among form, structure and space in the unique art work. Genius loci play very important role in the architectural creation - it represents a special and extra-ordinary urban locality and its architectural value in the historical, geographical and cultural context. The origin of Ostravice village within the historical frame concept of Moravia domain is the topic of this thesis. Other historical documents gave information about Bruneswerde as the Brno Castle. That means Brno Castle had to be founded not in Brno (as it has been consid-ered for many years) but it was located in Beskydy at Ostravice. The sacred city – Civitas Dei had been located in Bruneswerde region in early ages as the centre of European culture, education and spiritual life. Civitas Dei – divine Jerusalem in the transcription of St. Augustine's book De civitate Dei – is not only glorification of God and religious fantasy. It is also one of significant clues for recognition of historical architecture. The depiction of unknown settlement from the book of unde-fined origin is a superb testimony about extinct architectural works. They are legible from cadastral maps. Brno Castle - residence of nobility and power served shelter to St. Vojtěch, St. Prokop, St. Václav and St. Ludmila as it is obvious for the mentioned picture. Three major temples, three com-position axes symbolized by three towers on coins are in analogical relation to Brno triangle of four saints - the Saint family of Brno temples. Powerful ambitions of Brno City principals and clergy are inscribed into the urban structure in the way of composition relations which are legible to them who devoted themselves to the mystery of harmony. The absence of historical continuity affects personal attitudes and also identity of the whole community. The architecture truly reflects the past state of polis and it is eloquent even after its death. The architectural composition relations influence the natural environment for long time, longer than the architectural work existence. The geometric order of Renaissance Brno existence has not been in attention of architects so far. The features were discovered in characteristic paintings by Albrecht Durer. They are evidently secret works of the genius. A meaningful collaborator and follower in the extensive project was also his friend Jan Čert from Brno and lately from Vienna. His noble genealogy played a significant role in history of Silesia and Moravia for centuries. It is tendency to consider him as Austrian or even German architect. It is because of the fact that the genealogy tree of his noble family had roots in Moravia. It is supposed that Durer with Jan Čert´s support created the extraordinarily monumental architectural and urban works in Brno. A remarkable consensus in the urban composition of two squares and transition of traditional urban structure of Ostravice Civitas Dei into the modern Brno is also confirmed due to the identification of noble creators and owners, who were at the foundation, transformation and extinction of elements of the Moravian urban structure.
|
|
| |
|
| |
guest ::
