,
,
, Automatic Checkpointing to Debug a Sudoku Solver, p.92
,
, User-Perceived Performance Impact
,
97 6.2.1 Detecting Deadlocks in MPI Applications ,
,
103 7.7 Debugging of Distributed Systems From Message Traces, p.104 ,
, Fault Detection Based on Statistical Models
, We provided some examples that illustrate distributed i-RV. More thorough evaluation is needed on usability of distributed i-RV as well as on its performance. A case study shall be conducted on real-life bugs with developers trying our tool. We consider using the DbgBench dataset, Evaluation
, !finalNumberReceived, vol.617
,
,
, , vol.628
, // If this is an FinalVerdictNumber message, same thing but the scenario
, // remembers that the execution controller should be sent a quit request. 633 :: curMsg[self].type == FinalVerdictNumber -> 634 finalNumberReceived
, // If this is an event notification (presumably because of a prior
,
, // If no verdicts are expected for this event, let's send
, // actions and resume the execution, vol.643
, // If this is an NbMonitors messages, let's store the given number and 653
, // set the number of expected verdicts for every execution controller
, // This is cheating, since execution controllers are not known yet at
, // this point in the real protocol
, // upon the reception of hello messages of the execution controllers
, // Verdicts for an execution controller can be received before their
This makes the model simpler. 661 :: curMsg[self].type == NbMonitors -> 662 nbKnownMonitors = msgNumber(curMsg[self]) 663 for (i : 0 ,
, // If this is an acknowledgment for a request, let's continue handling
, // The event receivers are the monitors and the scenario
, // These are components that can request and receive events
, // This array is a list of these component, by order of arrival
, // of Hello messages by this execution controller)
, // If this is an Hello message 715 :: curMsg[self].type == Hello ->
, // If the joining component is a monitor or a scenario
, // identifier is stored in the list of event receivers 720 :: senderKind(curMsg[self]) == CMonitor || senderKind(curMsg[self]) == CScenario -> 721 eventReceivers
!(senderKind(curMsg[self]) == CMonitor || senderKind(curMsg, the message is ignored, vol.725 ,
, // If this is an event receiver, it is removed from the list of
, // known event receivers 735 :: senderKind(curMsg[self]) == CMonitor || senderKind(curMsg[self]) == CScenario -> 736 do 737 :: eventReceivers[i] == curMsg[self].sender -> 738 eventReceivers[i] = eventReceivers
!(senderKind(curMsg[self]) == CMonitor || senderKind(curMsg, the message is ignored, vol.746 ,
, // an event is generated, and either the message is final
, // if so, final verdict number will be sent. Otherwise, an expected
, // verdict number will be sent
, // -limited (if LIMIT_EVENTS is true), in which case eventsSent
, // counts the number of sent events (using the fact that
, // LIMIT_EVENTS = true = 1), and EVENT_MAX is the maximum
, // number of non-final events to generate
, // -or not (if LIMIT_EVENTS is false), in which case eventsSent
, // remains equal to zero (using the fact that
, // LIMIT_EVENTS = false = 0), to avoid changing the state of the
, // I'm not sure limiting the number of events is a great idea in this
, // model anyway, so we are probably better off keeping LIMIT_EVENTS
, (!LIMIT_EVENTS) || (eventsSent < EVENT_MAX)) -> eventsSent = eventsSent + ? LIMIT_EVENTS, vol.772
, // For each event receiver, either we sent an event notification
The number of monitors receiving the event notification ,
, // is computed and will be sent to the scenario. (i : 0 .. nEventReceivers -1) { 781 if 782 :: send(EventNotification, eventReceivers, p.783
, // If this is a regular request, the execution controller sends an
, // acknowledgment 798 :: curMsg[self].type == Request -> 799 send(Ack, curMsg[self].sender, 0)
, // We include a library that provides the following macros
,
, // at runtime. This allows smaller formulas
, // -defineLTL to define an LTL property with a name that can be reused in
,
,
, // Components receiving event notifications are monitors and scenarios, vol.825, p.827
, // Requests are sents by monitors and scenarios and received by execution controllers
, // Verdicts are sent by monitors to scenarios 838 defineAlwaysLTL(verdictsFromMonitorsAndToScenarios
,
,
,
, // These properties are only defined if HANDLE_VERIF_MESSAGE is true
, // These properties rely on checking values of the current messages at
, // Only curMsg[BUS] should be used, except for messages that are
, // broadcast / generated by the bus (Hello messages, NbMonitors)
, // It is hard to think about messages from other queues correctly without
, // doing mistakes. For instance, one could be tempted to write
,
,
,
,
, +)')dnl 31 undefine
, defineLTL', 'define('$1', 'apply_noteq_implies($2)') ('defineAlwaysLTL', 38 'define
, $ ( SPIN ) -a $ < 9 10 irv . pml : irv . m4 . pml constants . m4 betterltl . m4 11 $ ( M4 ) < $ < > $@ 12 13 . PHONY : clean 14 15 clean : 16 rm -rf $$
Defining liveness, Inf. Process. Lett, vol.21, issue.4, pp.181-185, 1985. ,
Recognizing safety and liveness, Distributed Computing, vol.2, issue.3, pp.117-126, 1987. ,
, AspectJ
Evolutionary deep learning-based energy consumption prediction for buildings, IEEE Access, vol.7, pp.1520-1531, 2019. ,
, Lectures on Runtime Verification -Introductory and Advanced Topics, vol.10457, 2018.
, Lectures on Runtime Verification -Introductory and Advanced Topics, vol.10457, 2018.
Decentralized asynchronous crash-resilient runtime verification, :15. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.59, pp.1-16, 2016. ,
Automaded: Automata-based debugging for dissimilar parallel tasks, Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010, pp.231-240, 2010. ,
Dynamic event generation for runtime checking using the JDI, Electr. Notes Theor. Comput. Sci, vol.70, issue.4, pp.21-35, 2002. ,
, Runtime Verification -5th International Conference, vol.8734, 2014.
How developers debug software the dbgbench dataset: poster, Proceedings of the 39th International Conference on Software Engineering, pp.244-246, 2017. ,
Practical memory checking with dr. memory, The 9th International Symposium on Code Generation and Optimization, pp.213-223, 2011. ,
Transparent dynamic instrumentation, Proceedings of the 8th International Conference on Virtual Execution Environments, pp.133-144, 2012. ,
Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pp.238-252, 1977. ,
, 5th USENIX Symposium on Networked Systems Design & Implementation, NSDI, 2008.
Elarva: A monitoring tool for erlang, Runtime Verification -Second International Conference, vol.7186, pp.370-374, 2011. ,
Model checking, 2001. ,
Frama-c -A software analysis perspective, Software Engineering and Formal Methods -10th International Conference, SEFM 2012, vol.7504, pp.233-247, 2012. ,
, , 2012.
A simple and practical approach to unit testing: The JML and junit way, ECOOP 2002 -Object-Oriented Programming, p.16 ,
, European Conference, pp.231-255, 2002.
, Runtime Verification -18th International Conference, vol.11237, 2018.
Automatic and configurable instrumentation of C programs with temporal assertion checkers, ACM/IEEE International Conference on Formal Methods and Models for Codesign, vol.13, pp.208-217, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01393418
Mop: an efficient and generic runtime verification framework, Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp.569-588, 2007. ,
Parametric trace slicing and monitoring, Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, pp.246-261, 2009. ,
, Comparison of checkpoint and restore solutions
Empirical studies of agile software development: A systematic review, Information & Software Technology, vol.50, issue.9, pp.833-859, 2008. ,
, Pdp-1 program library -DEC Debugging Tape, vol.21, 2019.
Efficient automated trace analysis: Examples with morphine, Electr. Notes Theor. Comput. Sci, vol.55, issue.2, pp.118-133, 2001. ,
Correctness proofs of compilers and debuggers : an approach based on structural operational semantics, 1992. ,
Opium: an extendable trace analyzer for prolog, The Journal of Logic Programming, vol.39, issue.1, pp.177-223, 1999. ,
, The DWARF debugging standard
Characterizing correctness properties of parallel programs using fixpoints, Automata, Languages and Programming, 7th Colloquium, Noordweijkerhout, The Netherland, vol.85, pp.169-181, 1980. ,
Monitoring decentralized specifications, Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp.125-135, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01653725
Can we monitor all multithreaded programs?, Colombo and Leucker [CL18], pp.64-89 ,
URL : https://hal.archives-ouvertes.fr/hal-01882414
The economics of artificial intelligence: Implications for the future of work, vol.10, 2018. ,
A review of reverse debugging, System, Software, SoC and Silicon Debug Conference (S4D), pp.1-6, 2012. ,
You should better enforce than verify, Runtime Verification -First International Conference, RV 2010, St. Julians, Malta, vol.6418, pp.89-105, 2010. ,
URL : https://hal.archives-ouvertes.fr/hal-00523653
What can you verify and enforce at runtime? STTT, vol.14, pp.349-382, 2012. ,
A tutorial on runtime verification, D: Information and Communication Security, vol.34, pp.141-175, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00853727
Reversible choreographies via monitoring in erlang, Distributed Applications and Interoperable Systems -18th IFIP WG 6.1 International Conference, DAIS 2018, Held as Part of the 13th International Federated Conference on Distributed Computing Techniques, vol.10853, pp.75-92, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01824635
Mpsoc zoom debugging: A deterministic record-partial replay approach, 12th IEEE International Conference on Embedded and Ubiquitous Computing, pp.73-80, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01006231
Striver: Stream runtime verification for real-time event-streams, Colombo and Leucker [CL18], pp.282-298 ,
Using runtime analysis to guide model checking of java programs, SPIN Model Checking and Software Verification, 7th International SPIN Workshop, vol.1885, pp.245-264, 2000. ,
, Held as Part of the Joint European Conferences on Theory and Practice of Software, vol.4959, 2008.
Verify your runs, Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, vol.4171, pp.374-383, 2005. ,
Software testing: Survey of the industry practices, MIPRO, pp.1449-1454, 2018. ,
The model checker SPIN, IEEE Trans. Software Eng, vol.23, issue.5, pp.279-295, 1997. ,
Synthesizing monitors for safety properties, Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, vol.2280, pp.342-356, 2002. ,
Defect detection efficiency: Test case based vs. exploratory testing, Proceedings of the First International Symposium on Empirical Software Engineering and Measurement, pp.61-70, 2007. ,
How do testers do it? an exploratory study on manual testing practices, Proceedings of the Third International Symposium on Empirical Software Engineering and Measurement, pp.494-497, 2009. ,
,
Interactive runtime verification -when interactive debugging meets runtime verification, 28th IEEE International Symposium on Software Reliability Engineering, pp.182-193, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01592671
Monitoring distributed systems, ACM Trans. Comput. Syst, vol.5, issue.2, pp.121-150, 1987. ,
Javamop: Efficient parametric runtime monitoring framework, 34th International Conference on Software Engineering, ICSE 2012, pp.1427-1430, 2012. ,
An on-line machine language debugger for OS/360, American Federation of Information Processing Societies: Proceedings of the AFIPS '69 Fall Joint Computer Conference, vol.35, pp.179-186, 1969. ,
Energy savings consumption on public wireless networks by SDN management, vol.24, pp.667-677, 2019. ,
Sree Nilakanta, and Xinxue (Shawn) Qu. The economics of public beta testing, Decision Sciences, vol.48, issue.1, pp.150-175, 2017. ,
Process planning optimization with energy consumption reduction from a novel perspective: Mathematical modeling and a dynamic programming-like heuristic algorithm, IEEE Access, vol.7, pp.7381-7396, 2019. ,
Transactions on aspect-oriented software development I, Transactions on Aspect-Oriented Software Development I, chapter Aspect Categories and Classes of Temporal Properties, pp.106-134, 2006. ,
A graphical development and debugging environment for parallel programs, Parallel Computing, vol.22, issue.13, pp.1747-1770, 1997. ,
AspectJ(tm): Aspect-oriented programming in Java, Objects, Components, Architectures, Services, and Applications for a Networked World, International Conference NetObject-Days, vol.2591, 2002. ,
Aspect-oriented programming, ECOOP'97 -Object-Oriented Programming, p.11 ,
, European Conference, vol.1241, pp.220-242, 1997.
Time, clocks, and the ordering of events in a distributed system, Commun, vol.21, issue.7, pp.558-565, 1978. ,
Undecidability of static analysis, LOPLAS, vol.1, issue.4, pp.323-337, 1992. ,
An integrated testing and debugging environment for parallel and distributed programs, 23rd EUROMICRO Conference '97, p.291, 1997. ,
Pin: building customized program analysis tools with dynamic instrumentation, Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, pp.190-200, 2005. ,
Large scale debugging of parallel tasks with automaded, Conference on High Performance Computing Networking, Storage and Analysis, vol.50, pp.1-50, 2011. ,
D3S: debugging deployed distributed systems, Crowcroft and Dahlin [CD08], pp.423-437 ,
Runtime assurance based on formal specifications, Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 1999, pp.279-287, 1999. ,
A brief account of runtime verification, J. Log. Algebr. Program, vol.78, issue.5, pp.293-303, 2009. ,
Unified debugging of distributed systems with recon, Proceedings of the 2011 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2011, pp.85-96, 2011. ,
Debugging at scale with allinea DDT ,
, Tools for High Performance Computing 2012 -Contributed Papers Presented at the 6th International Parallel Tools Workshop, pp.3-12, 2012.
A tutorial introduction to ADB, vol.21, 2019. ,
Decentralized runtime verification of LTL specifications in distributed systems, 2015 IEEE International Parallel and Distributed Processing Symposium, pp.494-503, 2015. ,
Communication and concurrency. PHI Series in computer science, 1989. ,
Reasoning in interval temporal logic, Logics of Programs, Workshop, vol.164, pp.371-382, 1983. ,
Scalable systems software -problem diagnosis in large-scale computing environments, Proceedings of the ACM/IEEE SC2006 Conference on High Performance Networking and Computing, p.88, 2006. ,
Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, vol.3253, pp.152-166, 2004. ,
Program instrumentation for debugging and monitoring with aspectc++, 5th International Symposiun on Object Oriented Real-Time Distributed Computing, pp.249-256, 2002. ,
Lightweight runtime checking of C programs with RTC, Computer Languages, Systems & Structures, vol.45, pp.191-203, 2016. ,
Rithm: a tool for enabling time-triggered runtime verification for C programs, Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE'13, pp.603-606, 2013. ,
Valgrind: a framework for heavyweight dynamic binary instrumentation, Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, pp.89-100, 2007. ,
In search of an understandable consensus algorithm, 2014 USENIX Annual Technical Conference, USENIX ATC '14, pp.305-319, 2014. ,
On the impact of code smells on the energy consumption of mobile applications, Information & Software Technology, vol.105, pp.43-55, 2019. ,
The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science, pp.46-57, 1977. ,
, Static Analysis -25th International Symposium, vol.11002, 2018.
Programming-Model Centric Debugging for multicore embedded systems / Debogage Interactif des systemes embarques multicoeur base sur le model de programmation, 2014. ,
URL : https://hal.archives-ouvertes.fr/tel-01010061
, Protocul Buffers website
Towards understanding interactive debugging, 2016 IEEE International Conference on Software Quality, Reliability and Security, QRS 2016, pp.152-163, 2016. ,
, Towards understanding interactive debugging, 2016.
, IEEE International Conference on Software Quality, Reliability and Security, pp.152-163, 2016.
PSL model checking and run-time verification via testers, FM, vol.4085, pp.573-586 ,
, , 2006.
Correctness of trap-based breakpoint implementations, Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.15-24, 1994. ,
Execution replay of parallel programs, Euromicro Workshop on Parallel and Distributed Processing, pp.429-434, 1993. ,
The energy and emergy of the internet, Tenth ACM Workshop on Hot Topics in Networks (HotNets-X), HOTNETS '11, p.9, 2011. ,
Debugar: Mixed dimensional displays for immersive debugging of distributed systems, Extended Abstracts of the 2018 CHI Conference on Human Factors in Computing Systems, CHI 2018, 2018. ,
Societal and ethical issues of digitization, Ethics Inf. Technol, vol.20, issue.2, pp.127-142, 2018. ,
Runtime verification with state estimation, RV, vol.7186, pp.193-207, 2011. ,
Are we overlooking some usability testing methods? A comparison of lab, beta, and forum tests, Behaviour & IT, vol.13, issue.1-2, pp.183-190, 1994. ,
Introduction to the special section on runtime verification, International Journal on Software Tools for Technology Transfer, vol.14, issue.3, pp.243-247, 2012. ,
Efficiency monitoring as a strategy for cost effective maintenance of induction motors for minimizing carbon emission and energy consumption, Rel. Eng. & Sys. Safety, vol.184, pp.193-201, 2019. ,
The developer coefficient ,
Meld: A real-time message logic debugging system for distributed systems, 5th IEEE Asia-Pacific Services Computing Conference, vol.2010, pp.59-66, 2010. ,
,
, Wordnet, vol.20, 2019.
, Wordnet definition of computer science, vol.20, 2019.
Vrisha: using scaling properties of parallel programs for bug detection and localization, Proceedings of the 20th ACM International Symposium on High Performance Distributed Computing, HPDC 2011, pp.85-96, 2011. ,