Login
Talks & Seminars
Title: Models of Time for Safety Critical Systems Partial vs. Total Order – Polychronous vs. Synchronous
Dr. Sandeep K. Shukla, Virginia Tech
Date & Time: November 19, 2014 11:00
Venue: Lecture Hall, B Block, 02nd/03rd Floor, Department of Computer Science and Engineering, Kanwal Rekhi (KReSIT) Building
Abstract:
In safety critical systems, accuracy of time is important if the activities of the system are time driven, and the notion of synchrony is based on the accuracy of time. The synchronization of clocks for such systems and protocols come at the cost of an overhead of running expensive synchronization algorithms. Moreover, in recent times, systems dependent on precise clock synchronization are vulnerable to cyber-attacks. In the context of embedded real-time systems models of time have been a subject of intense research in the past two decades. A distributed system endowed with strong clock synchronization mechanisms can view time as an approximately totally ordered (possibly infinite) set of instants. Assuming absence of clock drifting, robust clock synchronization protocols, and no cyber-attacks on clock synchronization, distributed algorithms and protocols can run safely in a time driven manner. Design and proof of such protocols are thus rendered simple due to linear or total order of time. However, today’s systems with multi-tasking, multi-threading, multi-core and distributed networked processing naturally require multiple local time references. This leads to a notion of polychronous time. Thus time is no longer unique or the same at all concurrently running entities, and have their own totally ordered instants as their local times. Therefore, these local instants are partially ordered. In a simple minded distributed system, one could schedule a step by step synchronous execution of the threads, so that they are always in lock step. Such a system preserves a logical total order of time across all the local times. But this amounts to barrier synchronization at every step – which degrades performance unnecessarily. Also, this requires a global coordinator – which is akin to global clock synchronization, and suffers from the same vulnerabilities and overheads. Thus polychronous notion of time frees us from the requirements of strong clock synchronization, and work at maximal performance in between synchronization points. The speeds of the concurrent entities do not need to be controlled except when it needs to block and wait for another computational thread to come to their mutual synchronization event. In order to free the programming model from synchronous timing model, and making systems robust to clock synchronization failure based attacks; we have been advocating polychronous model of computation for concurrent systems. However, we do not advocate that programmers design programs against this model manually, or prove correctness themselves. We propose a dataflow model of computation which describes only the intended computation as a set of concurrent data flows, and a program synthesis technique synthesizes multi-threaded code from such specifications. The generated code does not depend on clock synchronization, and each thread has local notion of time which are totally ordered themselves, and partially ordered globally. The correctness proof obligation is no longer with the implementer but with the modeler who would prove the properties on the concurrent dataflow model. The program synthesis engine of course has to be proven correct in order to claim correctness of the generated code from the model. In this talk we discuss the advantages of polychronous timing model for specifying security and safety critical systems, and derive the algorithms for code synthesis by analyzing the dependencies, concurrences, and pre-orders.
Speaker Profile:
Sandeep K. Shukla is a professor of Electrical and Computer Engineering at Virginia Tech. He is an IEEE Fellow, an ACM Distinguished Scientist and the Editor-in-Chief of the ACM Transactions on Embedded Computing Systems. He has published more than 200 conference papers, book chapters, and journal articles. He also co-edited or co-authored nine books. He is a recipient of the PECASE award, NSF CAREER award, Humboldt foundation’s Bessel award, an ASP-DAC best paper award etc. He is an IEEE computer society distinguished visitor and an ACM visiting speaker. He is currently working with the US Air Force to develop techniques and tools for multi-threaded code synthesis from polychronous specifications. Model of time in computational model is one of his major topics of interest. His other research areas are in probabilistic models of concurrency, application of formal methods to cyber security, safety-critical embedded system modeling and synthesis, formal verification, smart-grid and SCADA security models. He has also served as associated editors for IEEE Transactions on Computers, IEEE Embedded Systems Letters, IEEE Transactions on Industrial Informatics, and many other scholarly journals.
List of Talks

Webmail

Username:
Password:
Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback