|
|
Static Analysis Using Facebook Infer Focused on Errors in RCU-Based Synchronisation
Marek, Daniel ; Malík, Viktor (oponent) ; Vojnar, Tomáš (vedoucí práce)
Read Copy Update (RCU) is a synchronization mechanism, found mostly in the Linux kernel. Its sought-after features include almost zero overhead and high speed when reading shared memory. RCU has a set of rules of use, which need to be followed in order for the synchronization to work properly. To the best of our knowledge, there is no analyzer that sufficiently verifies if the RCU rules of use are adhered to. To overcome this, we propose a new analyzer, with the focus on finding violations in the use of RCU rules. The analyzer is based on static analysis and implemented as a module for the static analysis framework Facebook/Meta Infer. This platform was chosen because it provides scalability, which is needed when dealing with such an extensive software as the Linux kernel. The designed analyzer is capable of detecting multiple different ways in which the RCU usage rules can be broken, each causing either a race condition or a deadlock. It is also capable of generating warnings for situations when a deprecated function call is used or when the use of incompatible RCU reader and writer primitives is detected. The analyzer is the first of its kind. It may become a basis for future analyzer development in the field of Read Copy Update. Furthermore, it may be used as a test tool in the Linux kernel development cycle.
|
|
|
Static Analysis Using Facebook Infer Focused on Errors in RCU-Based Synchronisation
Marek, Daniel ; Malík, Viktor (oponent) ; Vojnar, Tomáš (vedoucí práce)
Read Copy Update (RCU) is a synchronization mechanism, found mostly in the Linux kernel. Its sought-after features include almost zero overhead and high speed when reading shared memory. RCU has a set of rules of use, which need to be followed in order for the synchronization to work properly. To the best of our knowledge, there is no analyzer that sufficiently verifies if the RCU rules of use are adhered to. To overcome this, we propose a new analyzer, with the focus on finding violations in the use of RCU rules. The analyzer is based on static analysis and implemented as a module for the static analysis framework Facebook/Meta Infer. This platform was chosen because it provides scalability, which is needed when dealing with such an extensive software as the Linux kernel. The designed analyzer is capable of detecting multiple different ways in which the RCU usage rules can be broken, each causing either a race condition or a deadlock. It is also capable of generating warnings for situations when a deprecated function call is used or when the use of incompatible RCU reader and writer primitives is detected. The analyzer is the first of its kind. It may become a basis for future analyzer development in the field of Read Copy Update. Furthermore, it may be used as a test tool in the Linux kernel development cycle.
|
|
|
Read-Copy-Update for HelenOS
Hraška, Adam ; Děcký, Martin (vedoucí práce) ; Podzimek, Andrej (oponent)
Rozšírenie viacjadrových procesorov zvýšilo záujem o škálovateľné synchronizačné primitíva ako je Read-Copy Update. Zatiaľčo RCU je populárne v monolitických kerneloch operačných systémov, doposiaľ nebolo nasadené v prostredí mikrokernelov. V práci navrhneme a implementujeme RCU pre mikrokernelový operačný systém HelenOS. Navyše preskúmame možnosti použitia RCU v HelenOSe a demonštrujeme užitočnosť RCU tak v kerneli ako aj v user space. Merania ukazujú, že implementované RCU poskytuje lineárnu škálovateľnosť RCU čitateľov a RCU vyžaduje omnoho nižšiu réžiu pri vstupe do chránenej sekcie ako bežné zámky a to i v ideálnom prípade pre zámky. RCU sme využili v user space na 2.6 násobné zrýchlenie tradičných zámkov. V kerneli RCU zabezpečilo lineárnu škálovateľnosť futexového podsystému. Powered by TCPDF (www.tcpdf.org)
|
|
|
Read-Copy-Update for HelenOS
Hraška, Adam ; Děcký, Martin (vedoucí práce) ; Podzimek, Andrej (oponent)
Rozšírenie viacjadrových procesorov zvýšilo záujem o škálovateľné synchronizačné primitíva ako je Read-Copy Update. Zatiaľčo RCU je populárne v monolitických kerneloch operačných systémov, doposiaľ nebolo nasadené v prostredí mikrokernelov. V práci navrhneme a implementujeme RCU pre mikrokernelový operačný systém HelenOS. Navyše preskúmame možnosti použitia RCU v HelenOSe a demonštrujeme užitočnosť RCU tak v kerneli ako aj v user space. Merania ukazujú, že implementované RCU poskytuje lineárnu škálovateľnosť RCU čitateľov a RCU vyžaduje omnoho nižšiu réžiu pri vstupe do chránenej sekcie ako bežné zámky a to i v ideálnom prípade pre zámky. RCU sme využili v user space na 2.6 násobné zrýchlenie tradičných zámkov. V kerneli RCU zabezpečilo lineárnu škálovateľnosť futexového podsystému. Powered by TCPDF (www.tcpdf.org)
|
host ::
RSS.