Keynote Speakers
Abstract
The bittide system is a recent approach to distributed
computing, designed to achieve synchronous execution at a
large scale without the need for a global clock or
traditional wall-clock synchronization. It aims to overcome
the complexity and expense of maintaining precise wall-clock
time in distributed systems, especially at datacenter scale.
The underlying mechanism of bittide uses feedback control to regulate the frequency of the hardware oscillators driving both computation and communication, in such a way as to ensure that all nodes operate in syntony. This allows applications to treat time as purely logical, and to make use of deterministic scheduling and programming methodologies across the entire datacenter.
In this talk we present an overview of the bittide system, discussing how the system works, mathematical formulations of the system behavior, and the consequences of logical synchrony for applications.
The underlying mechanism of bittide uses feedback control to regulate the frequency of the hardware oscillators driving both computation and communication, in such a way as to ensure that all nodes operate in syntony. This allows applications to treat time as purely logical, and to make use of deterministic scheduling and programming methodologies across the entire datacenter.
In this talk we present an overview of the bittide system, discussing how the system works, mathematical formulations of the system behavior, and the consequences of logical synchrony for applications.
Bio
Sanjay Lall is Professor of Electrical Engineering in the
Information Systems Laboratory at Stanford University. He
received a B.A. degree in Mathematics with first-class
honors in 1990 and a Ph.D. degree in Engineering in 1995,
both from the University of Cambridge, England. His research
group focuses on algorithms for control, optimization, and
machine learning. From 2018 to 2019 he was Director in the
Autonomous Systems Group at Apple. Before joining Stanford
he was a Research Fellow at the California Institute of
Technology in the Department of Control and Dynamical
Systems, and prior to that he was a NATO Research Fellow at
Massachusetts Institute of Technology, in the Laboratory for
Information and Decision Systems. He was also a visiting
scholar at Lund Institute of Technology in the Department of
Automatic Control. He has significant industrial experience
applying advanced algorithms to problems including satellite
systems, advanced audio systems, Formula 1 racing, the
America's cup, cloud services monitoring, and integrated
circuit diagnostic systems, in addition to several startup
companies. Professor Lall has served as Associate Editor for
the journal Automatica, on the steering and program
committees of several international conferences, and as a
reviewer for the National Science Foundation, DARPA, and the
Air Force Office of Scientific Research. He is the author of
over 130 peer-refereed publications. He is currently a
visiting researcher and director at Google.
Abstract
I will report our recent work on model-based formal design
of safety-critical embedded systems. With our approach, one
can build a graphical model for a system to be developed
with the combination of Simulink/Stateflow and AADL
(AADL+S/S), and then conduct extensive simulation. Any
AADL+S/S graphical model can be translated to an HCSP formal
model automatically, so that the translated HCSP formal
model can be verified using Hybrid Hoare Logic and its
theorem prover. To justify the correctness of the
translation, we define formal semantics of AADL+S/S and HCSP
respectively with HUTP (Higher-order Unifying Theories of
Programming), the correctness of the translation can
therefore be proved theoretically. Finally, we propose the
notion of approximate bisimulation for HCSP, and define a
set of refinement rules through which we can refine an HCSP
process into a piece of SystemC code or ANSI-C code, which
is approximate bisimilar to the original HCSP process. All
the above are supported by a tool chain called MARS. We
applied the above approach to design some real-world case
studies.
Bio
Naijun Zhan is a Boya distinguished professor in the School
of Computer Science of Peking University. He got his
bachelor degree and master degree both from Nanjing
University, and his PhD from Institute of Software Chinese
Academy of Sciences (ISCAS). Prior to join Peking
University, he worked at the Faculty of Mathematics and
Informatics, Mannheim University, Germany as a research
fellow, and afterwards worked at ISCAS as an associate
professor, a full professor, and a distinguished professor.
His research interests cover formal design of real-time,
embedded and hybrid systems, program verification, and so
on. He is in the editorial boards of Journal of Automated
Reasoning, Formal Aspects of Computing, Journal of Logical
and Algebraic Methods in Programming, Journal of Software,
Journal of Electronics, and Journal of Computer Research and
Development and so on, a member of the steering committees
of SETTA and MEMOCODE, the pc co-chairs of TACAS 2027, ICFEM
2025, FM 2021 and SETTA 2016, the general co-chairs of SETTA
2025, MEMOCODE 2019, MEMOCODE2018 and ICESS 2019, and serves
more than 100 international conferences program committees
e.g., CAV, RTSS, HSCC, FM, TACAS, EMSOFT and so on. He
published more than 150 papers in international leading
journals and conferences and 2 books, and edited 4
conference proceedings and 7 journal special issues. See
lcs.ios.ac.cn/~znj for more details.