Show simple item record

dc.contributor.advisorD'Souza, Deepak
dc.contributor.authorMukherjee, Suvam
dc.date.accessioned2018-06-29T08:16:32Z
dc.date.accessioned2018-07-31T04:39:18Z
dc.date.available2018-06-29T08:16:32Z
dc.date.available2018-07-31T04:39:18Z
dc.date.issued2018-06-29
dc.date.submitted2017
dc.identifier.urihttps://etd.iisc.ac.in/handle/2005/3777
dc.identifier.abstracthttp://etd.iisc.ac.in/static/etd/abstracts/4648/G28517-Abs.pdfen_US
dc.description.abstractConcurrent programs are pervasive owing to the increasing adoption of multi-core systems across the entire computing spectrum. However, the large set of possible program behaviors make it difficult to write correct and efficient con-current programs. This also makes the formal and automated analysis of such programs a hard problem. Thus, concurrent programs provide fertile grounds for a large class of insidious defects. Static analysis techniques infer semantic properties of programs without executing them. They are attractive because they are sound (they can guarantee the absence of bugs), can execute with a fair degree of automation, and do not depend on test cases. However, current static analyses techniques for concurrent programs are either precise and prohibitively slow, or fast but imprecise. In this thesis, we partially address this problem by designing efficient static analyses for concurrent programs. In the first part of the thesis, we provide a framework for designing and proving the correctness of data flow analysis for race free multi-threaded programs. The resulting analyses are in the same spirit as the \sync-CFG" analysis, originally proposed in De et al, 2011. Using novel thread-local semantics as starting points, we devise abstract analyses which treat a concurrent program as if it were sequential. We instantiate these abstractions to devise efficient relational analyses for race free programs, which we have implemented in a prototype tool called RATCOP. On the benchmarks, RATCOP was fairly precise and fast. In a comparative study with a recent concurrent static analyzer, RATCOP was up to 5 orders of magnitude faster. In the second part of the thesis, we propose a technique for detecting all high-level data races in a system library, like the kernel API of a real-time operating system (RTOS) that relies on ag-based scheduling and synchronization. Such races are good indicators of atomicity violations. Using our technique, a user is able to soundly disregard 99:8% of an estimated 41; 000 potential high-level races. Our tool detected 38 high-level data races in FreeRTOS (a popular OS in the embedded systems domain), out of which 16 were harmful.en_US
dc.language.isoen_USen_US
dc.relation.ispartofseriesG28517en_US
dc.subjectConcurrent Programsen_US
dc.subjectRace Free Programsen_US
dc.subjectThread-Local Semanticsen_US
dc.subjectRTOS Kernelen_US
dc.subjectL-DRFen_US
dc.subjectHigh-Level Data Racesen_US
dc.subjectRace-free Programsen_US
dc.subjectReal-time Operating Systemen_US
dc.subject.classificationComputer Scienceen_US
dc.titleEfficient Static Analyses for Concurrent Programsen_US
dc.typeThesisen_US
dc.degree.namePhDen_US
dc.degree.levelDoctoralen_US
dc.degree.disciplineFaculty of Engineeringen_US


Files in this item

This item appears in the following Collection(s)

Show simple item record