Runtime checking of refinement for concurrent software components

Abstract

Bu tezde, dosya sistemi ya da veritabanı depolama yünetim birimi gibiokoşut zamanlı ortamda şalıştırılan bir yazılım bileşeninin şalıştırılabilir birs cs s csbelirtime uygunluËunu denetlemek işin bir şalışma zamanı denetleme tekniËig c cs gsunulmaktadır. Belirtim her bir veri yapısı operasyonu işin atomik bir metotcsaËlamaktadır. Belirtim gerşekleştirimden ayrı olarak saËlanabileceËi gibig c s g ggerşekleştirimin atomik olarak şalışacak hale getirilmiş bir versiyonu da belir-c s cs sËtim olarak kullanılabilir. TekniËimiz iki aşamadan oluşmaktadır. Ilk aşamada,g s s sgerşekleştirim şalışma sırasında yürütme bilgisini bir günlüËe kaydedecekc s cs uu u ugËşekilde donatılır. Ikinci aşamada, ayrı bir sınama birimi günlüËe kaydedilmişs s u ug syürütme bilgisini kullanarak belirtimin bir ürneËini şalıştırır ve kayıtlı yürüt-uu o g cs uuËmenin belirtime ait yürütmeye uygunluËunu denetler. Ilgili tekniËin geneluu g guygulanabilirliËine ve ülşeklenebilirliËine, ayrıca denetlenen bileşenin koşutg oc g s szaman üzelliËine ve başarımına etkisinin en aza indirilmesine ünem verilmiştir.o g s o sSonuş olarak, koşut zamanlı programlar işin standart test yüntemine ünemlic s c o oyenilikler getiren bir doËrulama metodu geliştirilmiştir.g s sGerşekleştirimin belirtime uygunluËu arıtma adında bir doËruluk kri-c s g gteri olarak bişimsel-leştirilmiştir. Bu kritere güre gerşekleştirimin her birc s s o c syürütmesi işin ona denk belirtime ait bir yürütme bulunmalıdır. Yünteminuu c uu oyeni ozellikleri arasında en ünemlisi girdi/şıktı arıtma ve gürüş arıtma adındaü o c o usiki arıtma kriterinin tanımlanmasıdır. Boxwood adında endüstriyel ülşekteu ocveri yapısı gerşekleştirimleri işeren bir sistemin doËrulanması şalışmalarıc s c g csbu tanımlara motivasyon kaynaËı olmuştur. Girdi/şıktı arıtma ve gürüşg s c o usarıtmanın denetlenmesi VYRD (VerifYing concurrent programs by RuntimeReï¬nement-violation Detection) adlı doËrulama aracı bünyesinde gerşekleşti-g u c srilmiştir. VYRD, Boxwood sisteminin, Java sınıf kütüphanesinden birkaşs uu csınıfın doËrulanması amacıyla uygulanmıştır. Sonuşta, Boxwood sistemindeg s cdaha ünce tespit edilmeyen bir hataya ek olarak, Java sınıf kütüphanesindeo uuve test amaşlı yazılan ürneklerde daha ünceden bilinen hatalar yakalanmıştır.c o o sDeneyimler, ünerilen tekniËin pratikte uygun bir şalışma maliyeti olduËunuo g cs gortaya koymuştur.s

In this thesis, we present a runtime technique for checking that a con-currently accessed data structure implementation, such as a ï¬le system orthe storage management module of a database, conforms to an executablespeciï¬cation that contains an atomic method per data structure operation.The speciï¬cation can be provided separately or a non-concurrent, ?atom-ized? interpretation of the implementation can serve as the speciï¬cation.The technique consists of two phases. In the ï¬rst phase, the implementationis instrumented in order to record information into a log during execution.In the second, a separate veriï¬cation thread uses the logged information todrive an instance of the speciï¬cation and to check whether the logged exe-cution conforms to it. We paid special attention to the general applicabilityand scalability of the techniques and to minimizing their concurrency andperformance impact. The result is a lightweight veriï¬cation method thatprovides a signiï¬cant improvement over testing for concurrent programs.We formalize conformance to a speciï¬cation using the notion of reï¬ne-ment: Each trace of the implementation must be equivalent to some trace ofthe speciï¬cation. Among the novel features of our work are two variationson the deï¬nition of reï¬nement appropriate for runtime checking: I/O andview reï¬nement. These deï¬nitions were motivated by our experience withindustrial-scale concurrent data structure implementations in the Boxwoodproject, a novel storage infrastructure. I/O and view reï¬nement checkingwere implemented as a veriï¬cation tool named VYRD (VerifYing concurrentprograms by Runtime Reï¬nement-violation Detection). VYRD was appliedto the veriï¬cation of Boxwood, Java class libraries. It was able to detectpreviously unnoticed subtle concurrency bugs in Boxwood, the known bugsin the Java class libraries and manually constructed examples. Experimentalresults indicate that our techniques have modest computational cost.