Abstract
In mobile computing environments, logging systems are often used to record updates during device disconnection and logs are used in data synchronization on reconnection. Portable devices often have resource constraints and log truncation must be used to avoid log overflow. However, this method makes data synchronization vulnerable, due to information loss in truncating log files. Characteristic-entry logs record merely the most recent data access of each operation type per data item. They capture the minimum information needed to semantically resolve conflicting updates. They have been implemented in the MemorySafe system of Philips, a prototype distributed system supporting disconnected updates. In this paper, we present a formal model of characteristic-entry logs and investigate the relation between normal logs and characteristic-entry logs. We rigorously prove that characteristic-entry logs can be used in data synchronization, effectively in the same way as normal logs.
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
Qian, Y., Udink, R., Feijs, L.M.G.: A photo management system for future home environments. In: Proc. of International ITEA Workshop on Virtual Home Environments, pp. 93–101. Shaker, Aachen (2002)
van Loenen, E., de Jong, N., Dijk, E., van den Hoven, E., Qian, Y., Teixeira, D.: Phenom. In: Aarts, E., Marzanon, S. (eds.) The New Everyday, Views on Ambient Intelligence, pp. 302–303. Koninklijke Philips Electronics N.V. 010 Publishers (2003)
Pitoura, E., Bhargava, B.: Data Consistency in Intermittently Connected Distributed Systems. Knowledge and Data Engineering 11(6), 896–915 (1999)
Kistler, J.J., Satyanarayanan, M.: Disconnected Operation in the Coda File System. In: Proc. 13th ACM Symp. on Operating Systems Principles, vol. 25(5), pp. 213–225 (1991)
Pierce, B.C.: Unison File Synchronizor, http://www.cis.upenn.edu/~bcpierce/unison/
Balasubramaniam, S., Pierce, B.C.: What is a File Synchronizer? CSCI Technical Report #507. Indiana University (1998)
Ramsey, N., Csirmaz, E.: An algebraic approach to file synchronization. Technical Report TR-05-01, Harvard University, Dept. of Computer Science (May 2001)
Kumar, P., Satyanarayanan, M.: Log-Based Directory Resolution in the Coda File System. In: Proc. 2nd International Conference on Parallel and Distributed Information Systems, pp. 202–213 (1993)
Reiher, P., Heidemann, J., Ratner, D., Skinner, G., Popek, G.J.: Resolving File Conflicts in the Ficus File System. In: Proc. USENIX Summer Conference, pp. 183–195 (1994)
Guy, G.R., Heidemann, J.S., Mak, W., Page, T.W., Popek, G.J., Rothmeier, D.: Implementation of the Ficus Replicated File System. In: Proc. USENIX Summer Conference, CA, USA, June 1990, pp. 63–71 (1990)
Parker, D.S., Popek, G.J., Rudisin, G., Stoughton, A., Walker, B., Walton, E., Chow, J., Edwards, D., Kieser, S., Kline, C.: Detection of Mutual Inconsistency in Distributed Systems. IEEE Trans. Software Engineering 9(3), 240–246 (1983)
Davidson, S.B., Garcia-Molina, H., Skeen, D.: Consistency in Partitioned Networks. ACM Computing Surveys 17(3), 341–370 (1985)
Terry, D.B., Theimer, M.M., Petersen, K., Demers, A.N., Spreitzer, M.J., Hauser, C.H.: Managing Update Conflicts in Bayou, a Weakly Connected Replicated Storage System. In: Proc. 15th Symp. on Operating Systems Principles, pp. 172–183 (1995)
Qian, Y., Feijs, L.M.G., Udink, R.: Characteristic-entry logs in the MemorySafe Information System. In: Proc. 14th IASTED International Conference on Parallel and Distributed Computing and Systems, pp. 185–190. ACTA Press (2002)
Cellary, W., Gelenbe, E., Morzy, T.: Concurrency control in distributed database systems. North-Holland, Amsterdam (1988)
Spivey, J.M.: The Z Notation: a reference manual, 2nd edn. Prentice-Hall, Englewood Cliffs (1992)
Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)
Dijkstra, E.W., Scholten, C.: Predicate calculus and program semantics. Springer, Heidelberg (1990)
Diller, A.: Z: An Introduction to Formal Methods. John Wiley & Sons, Chichester (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Qian, Y. (2003). Formal Development of a Distributed Logging Mechanism Supporting Disconnected Updates. In: Dong, J.S., Woodcock, J. (eds) Formal Methods and Software Engineering. ICFEM 2003. Lecture Notes in Computer Science, vol 2885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39893-6_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-39893-6_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20461-9
Online ISBN: 978-3-540-39893-6
eBook Packages: Springer Book Archive