Progress estimation for model checker analysis execution in Progvis

Sammanfattning

In many modern applications, the presence of progress estimation at loading time issomething that has become almost expected by users. Many studies show that not havingany indication to the progress of the loading process even can degrade users’ opinions of aprogram or product. Therefore, especially during longer loading times, progress indicationis vital to satisfy users. Moreover, it has been shown to shorten the perceived waiting time,which also contributes to users’ improved opinions. This thesis focuses on implementingprogress estimation in Progvis, a tool used to teach concurrent programming to students.Progvis can be used to analyze user provided code, either manually or automatically.The automatic analysis is based on a model checker that performs an exhaustive searchof all possible execution paths. If there is an error in the code, it will terminate early,but if there are none, the code will have to run in its entirety. Therefore, the need forprogress indication became apparent.During the project, different solutions were explored. The experiments started outwith performing a manual analysis of the test code and execution time to try to findcorrelations. However, this yielded no result. Another method tried was modifying howthe model checker searches the code, but that too did not give any useful relations in thedata. When plotting how the edge count changed over time, the resulting relationshipappeared to be linear. Therefore statistical analysis was explored, and predicting thenecessary number of iterations required to reach a given number of edges. However, sinceno reliable way of calculating the final edge count was found, this approach was discarded.The final idea was to trace the relationship between explored and unexplored edges. Asthe resulting curve seemed similar to a quadratic equation, a function for polynomialregression was implemented. Based on the coefficients provided by the function, onecould calculate the zeros of the equation, giving an estimate of how many edges themodel checker will have explored when the unexplored edge count hits zero.In conclusion, the experiments resulted in regression functionality, combined with afunction to calculate the zeros of the equation returned by the regression. The progress isinitially a bit optimistic, but becomes more accurate further into the run, and the overheadfor the entire addition proved to be very small, about 0.09% of the total runtime. Theinitial poor accuracy seemed to be an okay compromise, given the small overhead, andthe fact that it improves over time. The calculated progress is displayed to the user as aprogress bar with a corresponding percentage.