We present Metis, a model-checking framework designed for versatile, thorough, yet configurable file system testing in the form of input and state exploration. It uses a nondeterministic loop and a weighting scheme to decide which system calls and their arguments to execute. Metis features a new abstract state representation for file-system states in support of efficient and effective state exploration. While exploring states, it compares the behavior of a file system under test against a reference file system and reports any discrepancies; it also provides support to investigate and reproduce any that are found. We also developed RefFS, a small, fast file system that serves as a reference, with special features designed to accelerate model checking and enhance bug reproducibility. Experimental results show thatMetis can flexibly generate test inputs; also the rate at which it explores file-system states scales nearly linearly across multiple nodes. RefFS explores states 3-28x faster than other, more mature file systems. Metis aided the development of RefFS, reporting 11 bugs that we subsequently fixed. Metis further identified 12 bugs from five other file systems, five of which were confirmed and with one fixed and integrated into Linux.

Can NLP assist in building formal models for verifying complex systems? We study this challenge in the context of parsing Network File System (NFS) specifications. We define a semantic-dependency problem over SpecIR, a representation language we introduce to model sentences appearing in NFS specification documents (RFCs) as semantic dependency structures, and present an annotated dataset of 1,198 sentences. We develop and evaluate semantic-dependency parsing systems for this problem. Evaluations show that even when using a state-of-the-art language model, there is significant room for improvement, with the best models achieving an F1 score of only 60.5 and 33.3 in the named-entity-recognition and dependency-link-prediction sub-tasks, respectively. We also release additional unlabeled data and other domain-related texts. Experiments show that these additional resources increase the F1 measure when used for simple domain-adaption and transfer-learning-based approaches, suggesting fruitful directions for further research.

Developing and maintaining a file system is time-consuming, typically requiring years of effort. Developers often test compliance with APIs such as POSIX with hand-written regression suites that, alas, examine only a fraction of a file system's state space. Conversely, formal model checking can explore vast state spaces efficiently, increasing confidence in the file system's implementation. Yet model checking is not currently part of file system development. Our position is that file systems should be designed a priori to facilitate model checking. To this end, we introduce MCFS, an architecture for efficient and comprehensive file-system model checking. MCFS relies on two new APIs that save and restore a file system's in-memory and on-disk state. We describe our earlier attempts at model-checking file systems, including unsuccessful or inefficient ones. Those attempts led us to develop VeriFS, which implements the new APIs. We illustrate MCFS's model-checking principles with VeriFS, a FUSE-based file system we were able to quickly develop with MCFS's help.

More applications nowadays use network and cloud storage; and modern network file system protocols support compounding operations---packing more operations in one request (e.g., NFSv4, SMB). This is known to improve overall throughput and latency by reducing the number of network round trips. It has been reported that by utilizing compounds, NFSv4 performance, especially in high-latency networks, can be improved by orders of magnitude. Alas, with more operations packed into a single message, partial failures become more likely---some server-side operations succeed while others fail to execute. This places a greater challenge on client-side applications to recover from such failures. To solve this and simplify application development, we designed and built TC-NFS, an NFSv4-based network file system with transactional compound execution. We evaluated TC-NFS with different workloads, compounding degrees, and network latencies. Compared to an already existing NFSv4 system that fully utilizes compounds, our end-to-end transactional support adds as little as ~1.1% overhead but as much as ~25× overhead for some intense micro- and macro-workloads.

In cloud computing environment, especially data-intensive systems, large amounts of datasets are stored in distributed data centres, and are often retrieved by users in different regions. To reduce the users' response time, replicating the popular datasets to multiple suitable data centres is an advisable choice, as tasks can access the datasets from a nearby site. Nevertheless, the dataset replicas' suitable storage placement selection is still an important issue that should be solved urgently from the response time constraint view, for the reason that too many replicas are infeasible in practice. In this paper, we first propose a comprehensive dataset response time estimation model, then present a replica placement model based on Steiner tree. After that, an approximate replica placement algorithm under a response time constraint in the cloud is given using Kruskal minimum spanning tree. At last, a practical and reasonable performance evaluation is designed and implemented. Both the theoretical analysis and simulations conducted on general (random) datasets show the efficiency and effectiveness of the proposed strategy in the cloud.

Distributed storage systems usually adopt replication for reliability and fast access. However, as the data volume grows, many large-scale storage systems are tending to employ erasure coding to reduce the storage overhead of replication while deliver the same reliability. Unfortunately, erasure coding could result in performance degradation due to less data locality and degraded reads. To trade off among reliability, performance and storage overhead at the same time, we propose FlexBM, a flexible dual-scheme block management approach. FlexBM supports both replication and erasure coding simultaneously, and applies them dynamically according to the recent data temperature. Erase coding is for cold data to reduce storage, while replication is for hot files so that applications can leverage data locality. To guarantee the same reliability as replication with fewer replicas, FlexBM models block placement with bipartite graphs. The prototype of FlexBM is implemented based on HDFS. The experimental results show that FlexBM succeeds in reducing the storage overhead even for a scenario with many small files without reliability compromising, and meanwhile, providing better data locality for frequently accessed datasets.

Graph has been widely used in complex network applications modeling, and the asynchronous graph processing model is superceding the BSP model because of its better convergence speed. However, the asynchronous GAS model proposed by PowerGraph usually results in irregular and unpredictable communication patterns as well as vertex-scale barriers, so it is difficult for programmers to optimize codes. To address these challenges, we propose LMCC, an improved message management approach including lazy pull-message model and vertex-oriented centralized cache, which can reduce communication cost in terms of message quantity, and reduce the number of computation iterations in turn, without compromising the accuracy of application results. Based on the deep investigation of the GAS phases, LMCC is designed to be totally transparent to user applications. Experimental results show that LMCC can deliver speedup for various types of graph computing benchmarks ranging from 129% to 271%.

A Hierarchical Weighted Voting System (HWVS) model is established to describe the Wireless Sensor Network (WSN) whose topology is cluster. Definitions about the reliability of the HWVS are presented. Based on universal generating function technique, an algorithm is suggested for evaluating the reliability of HWVS. In the algorithm, the u-functions of lower WVS and upper WVS are calculated separately, then the reliability of the whole HWVS is derived through the u-functions. The effects of system parameters (weights of sensor nodes, number of clusters, number of nodes in each cluster) on system reliability are analysed.

This paper presents a power allocation algorithm for optimizing network resources while considering the delay provisioning in multi-user relay networks. Our aim is to minimize the average power consumed by the relay nodes while satisfying the minimum Qos requirement of all users. Employing the convex optimization theory, we derive an optimal power allocation policy in a quasi-closed form and give two rules of how to select the relay nodes. Furthermore, a stochastic power method is developed to learn the fading state of the channels and carry out the optimal strategy immediately. Moreover, numerical results are provided to demonstrate the performance of the proposed resource allocation policies.