Eren Yildiz
Khakim Akhunov
Kasim Sinan Yildirim
ABSTRACT
Batteryless energy harvesting devices compute intermittently due to power failures that frequently interrupt the computational activity and lead to charging delays. To ensure functional correctness in intermittent computing, applications must exhibit several unique properties, such as guarantees for computational progress despite power failures and prevention of stale operations caused by charging delays. We observe that current software support for intermittent computing allows for checking only a fixed set of properties and leads to tightly coupled application and property-checking, thus hampering modularity, scalability, and maintainability.
In this paper, we present ARTEMIS, the first framework designed to facilitate flexible property checking of intermittent programs at runtime. ARTEMIS is developed based on techniques from the area of runtime monitoring, offers a specification language for specifying an open set of properties, and provides automatic generation of monitors responsible for checking the properties. Our evaluation showed that ARTEMIS achieves comparable efficiency to state-of-the-art solutions while significantly preventing failure scenarios through its monitoring capabilities.
- Efr32bg22 thunderboard kit. https://www.silabs.com/development-tools/thunderboard/thunderboard-bg22-kit?tab=overview, June 2023. Last accessed: June. 29, 2023.Google Scholar
- Joshua Adkins, Branden Ghena, Neal Jackson, Pat Pannuto, Samuel Rohrer, Bradford Campbell, and Prabal Dutta. The signpost platform for city-scale sensing. In 2018 17th ACM/IEEE International Conference on Information Processing in Sensor Networks (IPSN), pages 188--199. IEEE, 2018.Google ScholarDigital Library
- Mikhail Afanasov, Naveed Anwar Bhatti, Dennis Campagna, Giacomo Caslini, Fabio Massimo Centonze, Koustabh Dolui, Andrea Maioli, Erica Barone, Muhammad Hamad Alizai, Junaid Haroon Siddiqui, et al. Battery-less zero-maintenance embedded sensing at the mithræum of circus maximus. In Proceedings of the 18th Conference on Embedded Networked Sensor Systems, pages 368--381, 2020.Google ScholarDigital Library
- Saad Ahmed, Naveed Anwar Bhatti, Muhammad Hamad Alizai, Junaid Haroon Siddiqui, and Luca Mottola. Efficient intermittent computing with differential checkpointing. In Proceedings of the 20th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems, pages 70--81, 2019.Google ScholarDigital Library
- Khakim Akhunov and Kasim Sinan Yildirim. Adamica: Adaptive multicore intermittent computing. Proceedings of the ACM on Interactive, Mobile, Wearable and Ubiquitous Technologies, 6(3):1--30, 2022.Google ScholarDigital Library
- Anonymous. ARTEMIS Repository. https://, 2023.Google Scholar
- Abu Bakar, Rishabh Goel, Jasper de Winkel, Jason Huang, Saad Ahmed, Bashima Islam, Przemysław Pawełczak, Kasim Sinan Yildirim, and Josiah Hester. Protean: An energy-efficient and heterogeneous platform for adaptive and hardware-accelerated battery-free computing. In Proceedings of the 20th ACM Conference on Embedded Networked Sensor Systems, pages 207--221, 2022.Google ScholarDigital Library
- Abu Bakar, Alexander G Ross, Kasim Sinan Yildirim, and Josiah Hester. Rehash: A flexible, developer focused, heuristic adaptation platform for intermittently powered computing. Proceedings of the ACM on Interactive, Mobile, Wearable and Ubiquitous Technologies, 5(3):1--42, 2021.Google ScholarDigital Library
- Domenico Balsamo, Alex S Weddell, Anup Das, Alberto Rodriguez Arreola, Davide Brunelli, Bashir M Al-Hashimi, Geoff V Merrett, and Luca Benini. Hibernus++: a self-calibrating and adaptive system for transiently-powered embedded devices. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 35(12):1968--1980, 2016.Google ScholarDigital Library
- Ezio Bartocci, Yliès Falcone, Adrian Francalanza, and Giles Reger. Introduction to runtime verification. In Ezio Bartocci and Yliès Falcone, editors, Lectures on Runtime Verification - Introductory and Advanced Topics, volume 10457 of Lecture Notes in Computer Science, pages 1--33. Springer, 2018.Google ScholarCross Ref
- Naveed Anwar Bhatti and Luca Mottola. Harvos: Efficient code instrumentation for transiently-powered embedded sensing. In 2017 16th ACM/IEEE International Conference on Information Processing in Sensor Networks (IPSN), pages 209--220. IEEE, 2017.Google ScholarDigital Library
- Adriano Branco, Luca Mottola, Muhammad Hamad Alizai, and Junaid Haroon Siddiqui. Intermittent asynchronous peripheral operations. In Proceedings of the 17th Conference on Embedded Networked Sensor Systems, pages 55--67, 2019.Google ScholarDigital Library
- Jongouk Choi, Hyunwoo Joe, and Changhee Jung. Capos: Capacitor error resilience for energy harvesting systems. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 41(11):4539--4550, 2022.Google ScholarDigital Library
- Jongouk Choi, Larry Kittinger, Qingrui Liu, and Changhee Jung. Compiler-directed high-performance intermittent computation with power failure immunity. In 2022 IEEE 28th Real-Time and Embedded Technology and Applications Symposium (RTAS), pages 40--54. IEEE, 2022.Google ScholarCross Ref
- Alexei Colin and Brandon Lucia. Chain: Tasks and channels for reliable intermittent programs. In Proc. OOPSLA, pages 514--530, Amsterdam, Netherlands, 2016. ACM.Google ScholarDigital Library
- Alexei Colin and Brandon Lucia. Termination checking and task decomposition for task-based intermittent programs. In Proceedings of the 27th International Conference on Compiler Construction, pages 116--127, 2018.Google ScholarDigital Library
- Alexei Colin, Emily Ruppel, and Brandon Lucia. A reconfigurable energy storage architecture for energy-harvesting devices. In Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems, pages 767--781, 2018.Google ScholarDigital Library
- Christian Colombo and Gordon J. Pace. Runtime verification using LARVA. In Giles Reger and Klaus Havelund, editors, RV-CuBES 2017. An International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools, September 15, 2017, Seattle, WA, USA, volume 3 of Kalpa Publications in Computing, pages 55--63. EasyChair, 2017.Google Scholar
- Powercast Corp. Powercast hardware. http://www.powercastco.com, 2014. Last accessed: Dec. 10, 2020.Google Scholar
- Powercast Corp. Powercast hardware. https://www.powercastco.com/wp-content/uploads/2016/11/p2110-evb1.pdf, 2015. Last accessed: Dec. 10, 2020.Google Scholar
- Krzysztof Czarnecki and Simon Helsen. Classification of model transformation approaches. In Proceedings of the 2nd OOPSLA Workshop on Generative Techniques in the Context of the Model Driven Architecture, volume 45, pages 1--17. USA, 2003.Google Scholar
- Jasper de Winkel, Carlo Delle Donne, Kasim Sinan Yildirim, Przemyslaw Pawełczak, and Josiah Hester. Reliable timekeeping for intermittent computing. In Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems, pages 53--67, 2020.Google ScholarDigital Library
- Brad Denby, Emily Ruppel, Vaibhav Singh, Shize Che, Chad Taylor, Fayyaz Zaidi, Swarun Kumar, Zac Manchester, and Brandon Lucia. Tartan artibeus: A batteryless, computational satellite research platform. 2022.Google Scholar
- Harsh Desai, Matteo Nardello, Davide Brunelli, and Brandon Lucia. Camaroptera: A long-range image sensor with local inference for remote sensing applications. ACM Transactions on Embedded Computing Systems (TECS), 21(3):1--25, 2022.Google Scholar
- Eladio Domi, Beatriz Pérez, Ángel L Rubio, et al. A systematic review of code generation proposals from state machine specifications. Information and Software Technology, 54(10):1045--1066, 2012.Google ScholarDigital Library
- Ferhat Erata, Eren Yildiz, Arda Goknil, Kasim Sinan Yildirim, Ruzica Piskac, Jakub Szefer, and Gökçin Sezgin. Etap: Energy-aware timing analysis of intermittent programs. ACM Transactions on Embedded Computing Systems, 22(2):1--31, 2023.Google ScholarDigital Library
- Moritz Eysholdt and Heiko Behrens. Xtext: implement your language faster than the quick and dirty way. In Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion, pages 307--309, 2010.Google ScholarDigital Library
- Yliès Falcone, Srdan Krstic, Giles Reger, and Dmitriy Traytel. A taxonomy for classifying runtime verification tools. Int. J. Softw. Tools Technol. Transf., 23(2):255--284, 2021.Google ScholarDigital Library
- Arda Goknil and Kasim Sinan Yildirim. Toward sustainable iot applications: Unique challenges for programming the batteryless edge. IEEE Software, 39(5):92--100, 2022.Google ScholarDigital Library
- David Harel and Eran Gery. Executable object modeling with state-charts. In Proceedings of IEEE 18th International Conference on Software Engineering, pages 246--257. IEEE, 1996.Google ScholarDigital Library
- Josiah Hester, Kevin Storer, and Jacob Sorber. Timely execution on intermittently powered batteryless sensors. In Proceedings of the 15th ACM Conference on Embedded Network Sensor Systems, pages 1--13, 2017.Google ScholarDigital Library
- Natsuki Ikeda, Ryo Shigeta, Junichiro Shiomi, and Yoshihiro Kawahara. Soil-monitoring sensor powered by temperature difference between air and shallow underground soil. Proceedings of the ACM on Interactive, Mobile, Wearable and Ubiquitous Technologies, 4(1):1--22, 2020.Google ScholarDigital Library
- Gregor Kiczales, John Lamping, Anurag Mendhekar, Chris Maeda, Cristina Videira Lopes, Jean-Marc Loingtier, and John Irwin. Aspect-oriented programming. In Mehmet Aksit and Satoshi Matsuoka, editors, ECOOP'97 - Object-Oriented Programming, 11th European Conference, Jyväskylä, Finland, June 9-13, 1997, Proceedings, volume 1241 of Lecture Notes in Computer Science, pages 220--242. Springer, 1997.Google ScholarCross Ref
- Vito Kortbeek, Souradip Ghosh, Josiah Hester, Simone Campanoni, and Przemysław Pawełczak. Wario: efficient code generation for intermittent computing. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 777--791, 2022.Google ScholarDigital Library
- Vito Kortbeek, Kasim Sinan Yildirim, Abu Bakar, Jacob Sorber, Josiah Hester, and Przemysław Pawełczak. Time-sensitive intermittent computing meets legacy software. In Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems, pages 85--99, 2020.Google ScholarDigital Library
- Ivan Kurtev, Jozef Hooman, and Mathijs Schuts. Runtime monitoring based on interface specifications. In Joost-Pieter Katoen, Rom Langerak, and Arend Rensink, editors, ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, volume 10500 of Lecture Notes in Computer Science, pages 335--356. Springer, 2017.Google Scholar
- Brandon Lucia and Benjamin Ransford. A simpler, safer programming and execution model for intermittent systems. ACM SIGPLAN Notices, 50(6):575--585, 2015.Google ScholarDigital Library
- Kiwan Maeng, Alexei Colin, and Brandon Lucia. Alpaca: Intermittent execution without checkpoints. arXiv preprint arXiv:1909.06951, 2019.Google Scholar
- Kiwan Maeng and Brandon Lucia. Adaptive dynamic checkpointing for safe efficient intermittent computing. In 13th { USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 18), pages 129--144, 2018.Google Scholar
- Kiwan Maeng and Brandon Lucia. Adaptive low-overhead scheduling for periodic and reactive intermittent execution. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 1005--1021, 2020.Google ScholarDigital Library
- Amjad Yousef Majid, Carlo Delle Donne, Kiwan Maeng, Alexei Colin, Kasim Sinan Yildirim, Brandon Lucia, and Przemysław Pawełczak. Dynamic task-based intermittent execution for energy-harvesting devices. ACM Transactions on Sensor Networks (TOSN), 16(1):1--24, 2020.Google Scholar
- Jon Oldevik, Tor Neple, Roy Grønmo, Jan Aagedal, and Arne-J Berre. Toward standardised model to text transformations. In Model Driven Architecture-Foundations and Applications: First European Conference, ECMDA-FA 2005, Nuremberg, Germany, November 7-10, 2005. Proceedings 1, pages 239--253. Springer, 2005.Google ScholarDigital Library
- Benjamin Ransford, Jacob Sorber, and Kevin Fu. Mementos: System support for long-running computation on RFID-scale devices. In Proc. ASPLOS, Newport Beach, CA, USA, 2011. ACM.Google Scholar
- Emily Ruppel and Brandon Lucia. Transactional concurrency control for intermittent, energy-harvesting computing systems. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 1085--1100, 2019.Google ScholarDigital Library
- Dave Steinberg, Frank Budinsky, Ed Merks, and Marcelo Paternostro. EMF: Eclipse Modeling Framework. Pearson Education, 2008.Google ScholarDigital Library
- Texas Instruments. Msp430fr58xx, msp430fr59xx, msp430fr68xx, and msp430fr69xx family user's guide. http://www.ti.com/lit/ug/slau367o/slau367o.pdf, 2019. Last accessed: September 2019.Google Scholar
- Joel Van Der Woude and Matthew Hicks. Intermittent computation without hardware support or programmer intervention. In 12th { USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 16), pages 17--32, 2016.Google Scholar
- Kasim Sinan Yildirim, Amjad Yousef Majid, Dimitris Patoukas, Koen Schaper, Przemysław Pawełczak, and Josiah Hester. Ink: Reactive kernel for tiny batteryless sensors. In Proceedings of the 16th ACM Conference on Embedded Networked Sensor Systems, pages 41--53, 2018.Google ScholarDigital Library
- Eren Yildiz, Saad Ahmed, Bashima Islam, Josiah Hester, and Kasim Sinan Yildirim. Efficient and safe i/o operations for intermittent systems. In Proceedings of the Eighteenth European Conference on Computer Systems, pages 63--78, 2023.Google ScholarDigital Library
- Eren Yildiz, Lijun Chen, and Kasim Sinan Yildirim. Immortal threads: Multithreaded event-driven intermittent computing on {Ultra-Low-Power} microcontrollers. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22), pages 339--355, 2022.Google Scholar
- Eren Yildiz and Kasim Sinan Yildirim. Persistent timekeeping using harvested power measurements. In Proceedings of the 19th ACM Conference on Embedded Networked Sensor Systems, pages 572--574, 2021.Google ScholarDigital Library
Index Terms
- Adaptable Runtime Monitoring for Intermittent Systems
Recommendations
Runtime monitoring for safety of intelligent vehicles
DAC '18: Proceedings of the 55th Annual Design Automation ConferenceAdvanced driver-assistance systems (ADAS), autonomous driving, and connectivity have enabled a range of new features, but also made automotive design more complex than ever. Formal verification can be applied to establish functional correctness, but its ...
Efficient and Safe I/O Operations for Intermittent Systems
EuroSys '23: Proceedings of the Eighteenth European Conference on Computer SystemsTask-based intermittent software systems always re-execute peripheral input/output (I/O) operations upon power failures since tasks have all-or-nothing semantics. Re-executed I/O wastes significant time and energy and risks memory inconsistency. This ...
Partially Evaluating Finite-State Runtime Monitors Ahead of Time
Finite-state properties account for an important class of program properties, typically related to the order of operations invoked on objects. Many library implementations therefore include manually written finite-state monitors to detect violations of ...
Comments