Abstract
With the Distributed File System Replication component, DFS-R, as the central theme, we present selected protocol problems and validation methods encountered during design and development. DFS-R is currently deployed in various contexts; in Windows Server 2003-R2, Windows Live Messenger (Sharing Folders), and Windows Vista (Meeting spaces). The journey from an initial design sketch to a shipped product required mainly the dedicated effort of several testers, developers, program managers, and several others; but in some places cute problems related to distributed consensus and software model-checking emerged. This paper presents a few of these, including a distributed garbage collection problem, distributed consensus problems for reconciling tree-like data structures, using model-based test case generation, and the use of software model checking in design and development process.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Saito, Y., Shapiro, M.: Optimistic replication. ACM Comput. Surv. 37(1), 42–81 (2005)
Pierce, B.C., Vouillon, J.: Unison: A file synchronizer and its specification. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, p. 560. Springer, Heidelberg (2001)
Petersen, K., Spreitzer, M., Terry, D.B., Theimer, M., Demers, A.J.: Flexible update propagation for weakly consistent replication. In: SOSP, pp. 288–301 (1997)
Malkhi, D., Terry, D.B.: Concise Version Vectors in WinFS. In: Fraigniaud, P. (ed.) DISC 2005. LNCS, vol. 3724, pp. 339–353. Springer, Heidelberg (2005)
Teodosiu, D., Bjørner, N., Gurevich, Y., Manasse, M., Porkka, J.: Optimizing file replication over limited-bandwidth networks using remote differential compression. Technical report, Microsoft Research, MSR-TR-2006-157 (November 2006)
Lamport, L.: Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM 21(7), 558–565 (1978)
Baquero, C., Moura, F.: Improving causality logging in mobile computing networks. ACM Mobile Computing and Communications Review 2(4), 62–66 (1998)
Kang, B., Wilensky, R., Kubiatowicz, J.: The hash history approach for reconciling mutual inconsistency. In: ICDCS, pp. 670–677. IEEE Computer Society, Los Alamitos (2003)
Barnett, M., Grieskamp, W., Nachmanson, L., Schulte, W., Tillmann, N., Veanes, M.: Towards a Tool Environment for Model-Based Testing with AsmL. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 252–266. Springer, Heidelberg (2004)
Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: A model checker for concurrent software. In: Alur, R., Peled, D.A (eds.) CAV 2004. LNCS, vol. 3114, pp. 484–487. Springer, Heidelberg (2004)
Holzmann, G.J.: The Model Checker SPIN. IEEE Trans. Software Eng. 23(5), 279–295 (1997)
Jr., T.W.P., Guy, R.G., Heidemann, J.S., Popek, G.J., Mak, W., Rothmeier, D.: Management of Replicated Volume Location Data in the Ficus Replicated File System. In: USENIX Summer, pp. 17–30 (1991)
Allchin, J.E.: A Suite of Robust Algorithms For Maintaining Replicated Data Using Weak Consistency Conditions. In: Symposium on Reliability in Distributed Software and Database Systems, pp. 47–56 (1983)
Fischer, M.J., Michael, A.: Sacrificing Serializability to Attain High Availability of Data. In: PODS, pp. 70–75 (1982)
Oppen, D.C., Dalal, Y.K.: The clearinghouse: A decentralized agent for locating named objects in a distributed environment. ACM Trans. Inf. Syst. 1(3), 230–253 (1983)
Lin, S., Pan, A., Guo, R., Zhang, Z.: Simulating Large-Scale P2P Systems with the WiDS Toolkit. In: MASCOTS, pp. 415–424. IEEE Computer Society, Los Alamitos (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Bjørner, N. (2007). Models and Software Model Checking of a Distributed File Replication System. In: Jones, C.B., Liu, Z., Woodcock, J. (eds) Formal Methods and Hybrid Real-Time Systems. Lecture Notes in Computer Science, vol 4700. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75221-9_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-75221-9_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75220-2
Online ISBN: 978-3-540-75221-9
eBook Packages: Computer ScienceComputer Science (R0)