Submitted by Pedro Henrique Rodrigues (pedro.henriquer@ufpe.br) on 2015-03-05T18:45:35Z
No. of bitstreams: 2
jpso-master_rabbit_complete.pdf: 1450168 bytes, checksum: 081b9f94c19c494561e97105eb417001 (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-05T18:45:35Z (GMT). No. of bitstreams: 2
jpso-master_rabbit_complete.pdf: 1450168 bytes, checksum: 081b9f94c19c494561e97105eb417001 (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5)
Previous issue date: 2012-08-30 / Data-races are an important kind of error in concurrent shared-memory programs. Software model
checking is a popular approach to find them. This research proposes a novel approach to find races
that complements model-checking by efficiently reporting precise warnings during state-space
exploration (SSE): Rabbit. It uses information obtained across different paths explored during SSE
to predict likely racy memory accesses. We evaluated Rabbit on 33 different scenarios of race,
involving a total of 21 distinct application subjects of various sources and sizes. Results indicate
that Rabbit reports race warnings very soon compared to the time the model checker detects the
race (for 84.8% of the cases it reports a true warning of race in <5s) and that the warnings it reports
include very few false alarms. We also observed that the model checker finds the actual race
quickly when it uses a guided-search that builds on Rabbit’s output (for 74.2% of the cases it
reports the race in <20s).
Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/10891 |
Date | 30 August 2012 |
Creators | Oliveira, João Paulo dos Santos |
Contributors | Lima Filho, Fernando José Castor de, d’Amorim, Marcelo Bezerra |
Publisher | Universidade Federal de Pernambuco |
Source Sets | IBICT Brazilian ETDs |
Language | English |
Detected Language | English |
Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
Source | reponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE |
Rights | Attribution-NonCommercial-NoDerivs 3.0 Brazil, http://creativecommons.org/licenses/by-nc-nd/3.0/br/, info:eu-repo/semantics/openAccess |
Page generated in 0.0021 seconds