LATTE: An Object-based OracLe Framework for LineArizbility Testing of Multi-threaded SoftwarE

Description

p>Program testing is widely practiced in the industry to assure the quality of programs anddetect failures from them. Nowadays, many multithreaded programs are being developed. Critical failures such as memory corruption due to inconsistent concurrent accesses,deadlocks, and crashes are occasionally reported by the users of many importantmultithreaded programs such as MySQL and Tomcat. They show that the testingmethods applied to these programs still fail to deal with the real-world challenges.These failures are major threats when users perform their activities that rely on suchmultithreaded programs. All such critical failures are originated from unexpectedprogram states. Triggering these failures must firstly lead program executions intounexpected program states, which further require a reliable mechanism to determinewhether a program state is unexpected.Static analysis or model checking techniques are inherently imprecise to identifyunexpected program states from programs. Testing is an approach that executesprograms and can precisely report the presence of such critical concurrency bugs. Todetermine whether a program may result in an unexpected state, linearizability testingaims to check whether a concurrent trace follows the behavior of some sequential traceof the same program over the same input. Existing state-of-the-art automatedlinearizability testing techniques check the responses from methods, outputs from thetraces or assertion statements. Nonetheless, our preliminary experiment shows thatthese techniques miss to identify objects having states inconsistent with the states ofthe corresponding objects in the sequential trace counterparts. We have also found thatobjects in such unexpected states may lead the corresponding programs to crash orbecome deadlocking in some trace scenarios. New, precise, and automated techniquesthat effectively check and report unexpected states from execution traces of large-scaleprograms should be developed.This project aims at developing a novel LATTE framework to support object-statelinearizability testing to address all the above challenges in testing object-orientedmultithreaded programs. It formulates novel object-state models and conformancerelations to support the checking between objects in concurrent traces against objects intheir sequential trace counterparts. It systematically and recursively generateslinearizable traces, and exploits this characteristic to formulate novel strategies to selectobjects for object-state linearizability testing. It validates whether the trace prefixeshaving objects confirmed with object-state linearizability violations can trigger criticalfailures via randomized active testing. This project will also educate research studentsso that they can effectively contribute to the growth of the software industry aftergraduation.