Rabbit: A novel approach to find data-races during state-space exploration
Rabbit: A novel approach to find data-races during state-space exploration
| dc.contributor | Lima Filho, Fernando José Castor de | |
| dc.contributor | d’Amorim, Marcelo Bezerra | |
| dc.creator | Oliveira, João Paulo dos Santos | |
| dc.date | 2015-03-05T18:45:35Z | |
| dc.date | 2015-03-05T18:45:35Z | |
| dc.date | 2012-08-30 | |
| dc.identifier | OLIVEIRA, João Paulo dos Santos. Rabbit: a novel approach to find data-races during state-space exploration. Recife, 2012. 48 f. Dissertação (mestrado) - UFPE, Centro de Informática, Programa de Pós-graduação em Ciência da Computação, 2012. | |
| dc.identifier | https://repositorio.ufpe.br/handle/123456789/10891 | |
| dc.description | 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). | |
| dc.format | application/pdf | |
| dc.language | eng | |
| dc.publisher | Universidade Federal de Pernambuco | |
| dc.rights | Attribution-NonCommercial-NoDerivs 3.0 Brazil | |
| dc.rights | http://creativecommons.org/licenses/by-nc-nd/3.0/br/ | |
| dc.subject | Concorrency | |
| dc.subject | Software Verification | |
| dc.subject | Model Checking | |
| dc.subject | Race conditions | |
| dc.title | Rabbit: A novel approach to find data-races during state-space exploration | |
| dc.title | Rabbit: A novel approach to find data-races during state-space exploration | |
| dc.type | masterThesis |