https://ipads.se.sjtu.edu.cn/ 2026-05-18T21:15:06+00:00 https://ipads.se.sjtu.edu.cn/ https://ipads.se.sjtu.edu.cn/_media/wiki/dokuwiki.svg text/html 2023-10-14T13:31:11+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/atomfs?rev=1697290271&do=diff Formally Verified Concurrent File System (AtomFS) and CRL-H Framework News * 2019 Aug. 27: our AtomFS paper has been accepted by SOSP 2019 Overview Concurrent file systems are pervasive but hard to correctly implement and formally verify due to nondeterministic interleavings. We present AtomFS, the first formally-verified concurrent file system with our CRL-H framework, which provides linearizable interfaces to applications. We have successfully applied CRL-H to verify the linearizability … text/html 2020-08-21T08:46:06+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/catalyzer?rev=1597999566&do=diff Catalyzer: Sub-millisecond Startup for Serverless Computing with Initialization-less Booting News * 2020 March. 9: our Catalyzer paper has been accepted by ASPLOS 2020 Overview Serverless computing promises cost-efficiency and elasticity for high-productive software development. To achieve this, the serverless sandbox system must address two challenges: strong isolation between function instances, and low startup latency to ensure user experience. While strong isolation can be provided b… text/html 2012-01-06T04:25:29+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/chaos?rev=1325823929&do=diff CHAOS: Confidentiality and High-Assurance equipped Operating Systems The Problems Tamper-resistant software is vitally important to combat many challenges facing computer industry today . Examples include software copyright protection, digital right management (DRM), secure remote execution (e.g. grid computing) and software security. text/html 2016-02-22T13:57:12+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/cocytus?rev=1456149432&do=diff Cocytus Cocytus is a distributed in-memory key-value store which achieves both efficiency and availability by using hybrid erasure coding and replication. With low overhead for latency and throughput, it saves up to 46% memory compared to traditional primary-backup replications when tolerating two failures. An online recovery scheme is applied when failures are detected so that the whole system is able to serve key-value requests continuously. text/html 2013-03-01T05:55:00+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/coremu?rev=1362117300&do=diff COREMU : Scalable and Portable Parallel Emulation using Sequential Emulator COREMU is a parallel emulation framework for CMP systems that decouples the complexity of supporting parallel emulation from maturing a sequential emulator. It has now added deterministic replay support. text/html 2025-06-13T01:47:14+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/drtm?rev=1749779234&do=diff Efficient In-memory Transactional Processing Using New Advanced Hardware Overview The commercial availability of Intel’s Haswell processor suggests that hardware transactional memory (HTM), a technique inspired by database transactions, is likely to be widely exploited for commercial in-memory databases in the near future. Its features such as hardware-maintained read/write sets and automatic conflict detection naturally put forward a challenge on how HTM can successfully support concurrency c… text/html 2012-01-06T04:25:29+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/hang_survey?rev=1325823929&do=diff Hang Survey: A comprehensive study on software hang The Problems Software dependability is crucial to server and user applications, especially mission-critical ones. Unfortunately, software hang, a phenomenon of unresponsiveness, is still a major threat to software dependability. This kind of bug exists in many commodity software systems such as web browsers, database servers and office applications. text/html 2012-01-06T04:25:29+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/ica?rev=1325823929&do=diff ICA: Safe Binary Device Driver Reuse via User-level Binary Translation The Problems The maturity of new operating systems heavily depends on the enrichment and diversity of device drivers, which account for about 70% of commodity OS code base. Thus, it usually takes the major development and testing effort to support and integrate device drivers into a new text/html 2020-09-02T13:54:05+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/idas?rev=1599054845&do=diff IPADS Data Analytics Stack (IDAS) News * [Paper] August, 2020. Our paper “Fast RDMA-based Ordered Key-Value Store using Remote Learned Cache” was accepted by 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2020). * text/html 2012-01-06T04:25:29+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/ixen?rev=1325823929&do=diff The full iXen technical report is here. text/html 2012-01-06T04:25:30+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/lucos?rev=1325823930&do=diff LUCOS: Live Updating Contemporary Operating Systems The Problems Patches and upgrades are a part of everyday life for a contemporary operating system. Such patches and upgrades are frequently applied in order to plug security holes, add new features and enhance performance. Unfortunately, this process usually requires stopping and restarting a running operating system, which could constitute a major source of its loss of availability. However, for some long running and mission-critical systems… text/html 2012-01-06T04:25:30+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/mercury?rev=1325823930&do=diff Mercury: Combining Performance with Dependability Using Self-virtualization The Problems Virtualization is becoming a powerful and enabling technology for both research and daily use. However, the performance degradation it brings is not negligible. Evaluations on the two most popular virtual machine monitors (VMM), VMware and Xen, shows performance overhead from several percents to tens of percents for various workloads. IO intensive workloads suffer much more serve performance degradation th… text/html 2012-01-06T04:25:30+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/ovm?rev=1325823930&do=diff OVM: Type-safe, Object-oriented Virtual Machine Monitors The Problems System virtualization has recently gained a resurgent interest and made system research more relevant. Evidences include many systems and innovations, as well as commercial successes. It is claimed that VMMs have become text/html 2013-03-16T02:36:37+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/parallel_vm_migration?rev=1363401397&do=diff Parallelizing Live Migration of Virtual Machines Live VM migration is one of the major primitive operations to manage virtualized cloud platforms. However, with the increasing amount of resources configured to a single VM, this process may be extremely time-consuming, causing notable disruption to the running services. In this project, we investigate how this process could be parallelized on commodity multicore platforms. text/html 2012-01-06T04:25:30+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/polus?rev=1325823930&do=diff POLUS: A POwerful Live Updating System The Problems The scale of software has increased dramatically in the past two decades, so do the bugs and security vulnerabilities. Despite progress made in software engineering with better programming support, improved developing models and more effective testing tools, it is undeniable that software is still far from perfect, and this trend is likely to continue. Consequently, there has been an increasing number of software updates to fix bugs, close vu… text/html 2014-10-23T12:27:55+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/prwlock?rev=1414067275&do=diff Passive Reader-Writer Lock : Scalable Read-mostly Synchronization Using Passive Reader-Writer Locks Passive reader-writer lock (Prwlock) is a reader writer lock designed for scalable read-mostly synchronization. It provides scalable read-side performance as well as small writer latency for TSO architectures. It is mainly implemented in kernel mode. We use it to protect address space tree based on Linux 3.8. text/html 2024-06-06T11:41:10+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/reffs?rev=1717674070&do=diff Formally Verified Concurrent File System (RefFS) and MoLi Framework News * March 21, 2024: our RefFS paper has been conditionally accepted by OSDI 2024 Overview RefFS is the first concurrent file system that guarantees both liveness and safety, backed by a machine-checkable proof in Coq. Unlike earlier concurrent file systems, RefFS provably avoids termination bugs such as livelocks and deadlocks, through its innovative introduction and use of the dynamically layered definite releases speci… text/html 2012-04-19T02:36:56+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/shepherd?rev=1334803016&do=diff Shepherd: VMM-based Process Shepherding The Problems Security and reliability have become two of the biggest problems facing contemporary computing systems. These systems are fragile and always sus- ceptible to various attacks, intrusions and abuses. One of the major reasons for such problems is that contemporary operating systems are designed and optimized for openness, functionality and efficiency, but not for security and reliability. Processes in a contemporary operating system are usually… text/html 2014-08-22T02:32:02+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/ssmalloc?rev=1408674722&do=diff SSMalloc: A Low-latency, Locality-conscious Memory Allocator with Stable Performance Scalability The Problems The efficiency of memory allocator is a key factor affecting application performance. However, most state-of-art memory allocators only manages to scale well with a small number of application threads. They cannot maintain stable scalability and locality when the number of threads exceeds the number of cores, which may be common in nowadays software. We believe that performance stabili… text/html 2012-01-06T04:25:30+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/vicover?rev=1325823930&do=diff Motivation Crashed dump, or core dump, is the typical routine automatically executed on system crash by the system administrator, to save the failure context of the system into persistent storage, for future offline debugging and analysis. After core dump completes, the administrator can restart the system with the reclaimed memory as reboot-based recovery. text/html 2020-09-17T12:38:58+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/wukong?rev=1600346338&do=diff Fast and Concurrent Query Processing on Big (Linked) Data News * 2019 May 23: our wukong w/ live migration paper has been accepted by USENIX ATC 2019 * 2018 Apr. 19: our wukong w/ GPU paper has been accepted by USENIX ATC 2018 * 2017 Oct. 27: the first release (v0.1.0) of wukong @github. text/html 2020-10-15T08:14:42+00:00 Anonymous (anonymous@undisclosed.example.com) https://ipads.se.sjtu.edu.cn/pub/projects/xstore?rev=1602749682&do=diff XSTORE: efficient RDMA-based ordered key-value store using learned cache Overview XSTORE is an RDMA-enabled ordered key-value store targeted at a client-sever setting. Specifically, the server has an in-memory B+Tree; and the client uses one-sided RDMA READs to traverse the B+Tree. To accelerate the lookup, we deploy a learned cache (xcache) at the client to accomplish the traversal in one round-trip (if the learned cache is all cached). Even if the xcahe is not cached, XStore client only need…