کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
6875267 1441593 2018 24 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Some trade-offs in reducing the overhead of assertion run-time checks via static analysis
ترجمه فارسی عنوان
بعضی از معاملات در کاهش سربار چک های زمان ادعایی از طریق تجزیه و تحلیل استاتیک
کلمات کلیدی
ترجمه چکیده
تعدادی از رویکردهای برای کمک به برنامه نویسان در تشخیص رفتارهای برنامه نادرست بر مبنای ترکیبی از ساختارهای سطح زبان (مانند ادعاهای / قراردادهای سطح رویه ها، اظهارات برنامه نقطه یا نوع تدریجی) با تعدادی از ابزارهای مرتبط (مانند تحلیلگرهای کد و چارچوب تایید زمان اجرا) که به طور خودکار اعتبار چنین سازه ها را بررسی می کند. با این حال، این ساختارها و ابزارها اغلب به علت سربار اضافی زمان اجرا، محدودیت بیان و / یا محدودیت در کارآیی ابزارها به طور کامل در عمل به کار نمی روند. چارچوب تایید که ترکیبی از تکنیک های تایید استاتیک و پویا است و بر اساس انتزاع ارائه می دهد، بالقوه برای بروز این شکاف است. در این مقاله به بررسی اثربخشی تفسیر انتزاعی در تشخیص بخش هایی از مشخصات برنامه می پردازیم که می تواند به طور واقعی به درست یا غلط ساده و همچنین کاهش هزینه های چک در زمان اجرا مورد نیاز برای بخش های باقی مانده از این مشخصات باشد. شروع با معناشناسی برای برنامه هایی که با تکرار ادعا و ساده کردن ادعای بر اساس تجزیه و تحلیل آماری استاتیک به دست آمده از طریق تفسیر انتزاعی، ما پیشنهاداتی را ارائه می کنیم و برخی از اصطلاحات عملی را برای بررسی حالت ها، ارائه می کنیم. هر کدام از اینها نشان دهنده یک توافق بین عمق حاشیه نویسی کد، کاهش سرعت اجرای برنامه و ایمنی برنامه است. سپس این دو حالت را در دو سناریوی معمولی، کتابخانه ای مورد بررسی قرار می دهیم. ما همچنین روشهای مبتنی بر تحول برنامه را برای استفاده از معانی سنجش زمان اجرا برای بهبود دقت تجزیه و تحلیل پیشنهاد می کنیم. در نهایت، ما به طور تجربی به بررسی عملکرد این تکنیک ها می پردازیم. آزمایشات ما مزایا و هزینه های هر یک از حالت های بررسی فرضیه را نشان می دهد، همچنین مزایای حاصل از تجزیه و تحلیل و تحولات پیشنهاد شده در این سناریوها را نشان می دهد.
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش مقاله
بعضی از معاملات در کاهش سربار چک های زمان ادعایی از طریق تجزیه و تحلیل استاتیک
چکیده انگلیسی
A number of approaches for helping programmers detect incorrect program behaviors are based on combining language-level constructs (such as procedure-level assertions/contracts, program-point assertions, or gradual types) with a number of associated tools (such as code analyzers and run-time verification frameworks) that automatically check the validity of such constructs. However, these constructs and tools are often not used to their full extent in practice due to excessive run-time overhead, limited expressiveness, and/or limitations in the effectiveness of the tools. Verification frameworks that combine static and dynamic verification techniques and are based on abstraction offer the potential to bridge this gap. In this paper we explore the effectiveness of abstract interpretation in detecting parts of program specifications that can be statically simplified to true or false, as well as in reducing the cost of the run-time checks required for the remaining parts of these specifications. Starting with a semantics for programs with assertion checking, and for assertion simplification based on static analysis information obtained via abstract interpretation, we propose and study a number of practical assertion checking “modes,” each of which represents a trade-off between code annotation depth, execution time slowdown, and program safety. We then explore these modes in two typical, library-oriented scenarios. We also propose program transformation-based methods for taking advantage of the run-time checking semantics to improve the precision of the analysis. Finally, we study experimentally the performance of these techniques. Our experiments illustrate the benefits and costs of each of the assertion checking modes proposed, as well as the benefits obtained from analysis and the proposed transformations in these scenarios.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 155, 1 April 2018, Pages 3-26
نویسندگان
, , ,