%0 Conference Paper
%B Fast Abstract in Latin-American Symposium on Dependable Computing
%D 2011
%T Model Checking a Decentralized Storage Deduplication Protocol
%A João Paulo
%A José Orlando Pereira
%C São José dos Campos, Brazil
%P 1
%X <p>Deduplication of live storage volumes in a cloud computing environment is better done by post-processing: by delaying discovery and removal of duplicate data after I/O requests have been concluded, impact in latency can be minimized. When compared to traditional deduplication in backup systems, which can be done in-line and in a centralized fashion, distribution and concurrency lead to increased complexity. This paper outlines a deduplication algorithm for a typical cloud infrastructure with a common storage pool and summarizes how model-checking with the TLA+ toolset was used to uncover and correct some subtle concurrency issues.</p>
%8 April
%> https://haslab.uminho.pt/sites/default/files/jtpaulo/files/pp09.pdf