VLDB 2026 Research / reviewers in the wild / expert
Yu Bai 0003
dblp:03/6325-3
· DBLP profile ↗
9ranked-venue papers
5as first author
3since 2021 · last 2021
—ORCID · conflict
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 5 · 4 first-author · 2 since 2021Systems, architecture and hardware · 4 · 2 first-author · 2 since 2021Theory of computation · 2 · 2 first-authorApplied, interdisciplinary, general and emerging computing · 1 · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2021 | Synthesis of Heterogeneous Dataflow Models from Synchronous SpecificationsabstractThe synthesis of distributed embedded systems by desynchronization starts from a synchronous model and keeps its functional behavior while generating a corresponding dataflow process network (DPN). This method supports the modeling of dynamic behaviors while avoiding the problems like deadlocks and buffer overflows in DPNs. However, a DPN can be heterogeneous in the sense that different nodes may exhibit either static or dynamic behaviors. An efficient synthesis method should automatically generate implementations by exploiting this heterogeneity.In this paper we improve the desynchronization process by exploiting synchronous components with various input/output behaviors which can then be desynchronized to a heterogeneous DPN where each node can be scheduled and executed accordingly. Moreover, a synthesis tool chain is developed to automatically synthesize the heterogeneous DPN to the open computing language (OpenCL) based implementation that can be deployed on various commercial off-the-shelf (COTS) target platforms. Omair Rafique, Yu Bai 0003, Klaus Schneider 0001, Guangxi Yan |
COMPSAC | 2 |
| 2021 | A Model-based Design Flow for Asynchronous Implementations from Synchronous SpecificationsabstractThe synthesis of distributed embedded systems from dataflow models like Kahn Process Networks (KPN) has to deal with particular problems like absence of deadlocks and buffer overflows. However, the verification of the absence of these problems for a KPN model is in general not decidable. Starting with synchronous models, desynchronization avoids such design difficulties by generating sound dataflow networks by correctness of construction. In this paper, we present a design flow following such an approach. Our design flow differs from previous work in the following aspects: The synchronous models are specified by an imperative synchronous language and are therefore better suited for control-intensive applications. Verification of desynchro-nization criteria is carried out efficiently with the help of model checking and SAT-solving, ensuring the compliance of the functional behavior. Qualified code is translated automatically into the KPN model. Finally, the KPN model is automatically synthesized to the open computing language (OpenCL) based implementation which is platform independent and can be executed on various commercial off-the-shelf target platforms. Yu Bai 0003, Omair Rafique, Klaus Schneider 0001 |
DATE | 1 |
| 2021 | Efficient Implementation of Heterogeneous Dataflow Models using Synchronous IO PatternsabstractThe synthesis of distributed embedded systems based on desynchronization is attractive since it preserves the functional behavior of the synchronous model while avoiding the verification of the absence of problems like deadlocks and buffer overflows. In this paper, we improve the desynchronization process by introducing synchronous components with various input/output (IO) patterns which can then be desynchronized to a heterogeneous dataflow process network (DPN) where each node can be scheduled and executed accordingly. We further designed a synthesis tool chain that automatically synthesizes the heterogeneous DPN to the open computing language (OpenCL) based implementation which is platform-independent and can be deployed on various commercial off-the-shelf (COTS) target platforms. Omair Rafique, Yu Bai 0003, Klaus Schneider 0001, Guangxi Yan |
DSD | 2 |
| 2014 | Isochronous networks by constructionabstractWhile synchronous system models have many advantages over asynchronous models concerning verification and validation, many implementation platforms do not provide efficient means for synchronization. For this reason, we consider a design flow that starts with a synchronous system model that is then transformed into an asynchronous one for synthesis. In essence, it partitions the synchronous system into a set of asynchronous components that communicate with each other via FIFO buffers. Of course, the synthesized system still has to behave as the original synchronous model, i.e., for each variable exactly the same flow of data values must be observed and only the membership to synchronous reaction steps is no longer explicitly given. In this paper, we prove that this correctness guarantee is given provided that (1) each component knows which of the input values have to be used for the next reaction (endochrony), (2) each component is able to perform the reaction (constructiveness), and (3) components agree on the clocks of their shared variables (isochrony/clock-consistency). Yu Bai 0003, Klaus Schneider 0001 |
DATE | 1 |
| 2014 | From clock-driven to data-driven modelsabstractClock/time-driven models are powerful abstractions of real-time systems, as e.g., provided by the synchronous models of computation which lend themselves well for simulation and verification. At every clock cycle, new inputs are read, computations are performed in zero-time, and results are immediately/synchronously communicated between components. However, such zero-time idealizations are not realistic since computation and communication finally takes time in implementations. For implementations, data-driven execution models have the advantage to impose no timing constraints other than arrival of input data, and thus, these models are perfectly suited for distributed or other kinds of asynchronous implementations. For this reason, modern model-based design flows consider the desynchronization of synchronous models for system synthesis which is possible for the subclass of endochronous systems only. While definitions of endochrony were considered for years, it is shown in this paper how to efficiently verify endochrony by SAT solving. Our procedure consists of two steps: In the first step, we introduce buffers to the interface of a clock-driven component, so that its inputs can arrive at different points of time. After this step, clocks of signals are viewed as ‘instructions’ telling the component which input values have to be consumed for the current reaction.We call such components clock-scheduled. In the second step, we remove the clocks from the interface of the clock-scheduled components, so that the component may now become nondeterministic. We prove in this paper that a synchronous component is endochronous, if and only if the clock signals can be safely removed in this step without destroying determinism. Based on this result, we present a decision procedure based on symbolic system representations to check whether components are endochronous. Preliminary experimental results show the effectiveness of our method. Yu Bai 0003, Klaus Schneider 0001, Nikita Bhardwaj Haupt, Badarinath Katti, Tania Shazadi |
MEMOCODE | 1 |
| 2014 | Reducing the Communication of Message-Passing Systems Synthesized from Synchronous ProgramsabstractThis paper presents a method to translate a given synchronous system to a multithreaded system where process nodes communicate via channels with each other. It is well-known that the reduction of communication has been identified to be a crucial key for efficient utilization of multiprocessor systems. For this reason, we first use synchronous elastic design methods to generate a distributed/multithreaded system from a synchronous system, and then, reduce communication overhead between the obtained process nodes. Our benchmarks show that we can save up to 67.5% of communication costs using our method and can achieve an average speed-up of up to 1.09. Daniel Baudisch, Yu Bai 0003, Klaus Schneider 0001 |
PDP | 2 |
| 2014 | Passive code in synchronous programsabstractThe synchronous model of computation requires that in every step, inputs are read and outputs are synchronously computed as the reaction of the program. In addition, all internal variables are updated in parallel even though not all of these values might be required for the current and the future reaction steps. To avoid unnecessary computations, we present a compile-time optimization procedure that computes for every variable a condition that determines whether its value is required for current or future computations. In this sense, our optimizations allow us to identify passive code that can be disabled to avoid unnecessary computations and therefore to reduce the reaction time of programs or their energy consumption. Jens Brandt 0001, Klaus Schneider 0001, Yu Bai 0003 |
ACM Trans. Embed. Comput. Syst. | 3 |
| 2012 | Preservation of LTL properties in desynchronized systemsabstractThe synchronous programming model is perfect for modeling, simulation, verification and implementation of reactive systems. While this paradigm can be directly implemented as hardware circuits, multithreaded software implementations are typically based on asynchronous threads. For this reason, an efficient multithreaded software implementation of a synchronous program requires a so-called desynchronization that could however potentially violate the already verified properties of the synchronous program. In this paper, we therefore present a theory to check whether properties verified for a synchronous system are preserved by a desynchronization. In particular, we prove a theorem based on directed-flow equivalence that specifies the requirements of delay relations among system variables that a desynchronization has to meet. Yu Bai 0003, Jens Brandt 0001, Klaus Schneider 0001 |
MEMOCODE | 1 |
| 2011 | SMT-based optimization for synchronous programsabstractIn this paper, we present several optimization techniques to improve the runtime and size of the code generated from synchronous programs. These optimizations work on extended finite state machines (EFSMs) that can be used as intermediate representation for any synchronous system. Our optimizations consists of two phases: First, local optimization guides the EFSM generation and considers the states and edges separately. Second, global optimization is based on a dataflow analysis of the entire EFSM. For both phases, we employ an SMT (Satisfiability Modulo Theories) solver to verify the individual optimization steps. Our experiments show the potential of the presented optimizations: optimized programs generally have a smaller size and a better run-time performance. Yu Bai 0003, Jens Brandt 0001, Klaus Schneider 0001 |
SCOPES | 1 |