数据备份系统是互联网服务的基本组成单元之一,是提供高可用服务的重要保障。随着服务规模的不断扩大,为了能够快速响应不同地区用户的请求,许多互联网服务提供商将数据副本放置到靠近用户的数据中心。然而,在跨地域的数据中心之间进行备份强同步会造成用户请求时延的陡然上升。为解决这一冲突,近年来,一些弱一致性模型相继被提出并被使用在上述场景中。虽然弱一致性模型具有性能优势,但却不能时刻保证上层应用的正确性。因此,结合真实场景中应用的客观需求,研究人员们开始关注混合一致性模型的研究和应用。混合一致性模型可以允许互联网服务的设计者在一致性、系统性能、服务正确性等方面做出权衡,同时也为设计者们带来了编程的负担和挑战。这是因为较弱的一致性模型提供的语义与强一致性的语义不同,编程人员需要确保在强同步缺省的情况下,服务并行执行仍然能够满足应用的语义需求(例如满足状态收敛性或满足特定不变量)。为了解决以上问题,首先,本文提出了一个细粒度一致性模型和相应的编程语言,并给出了相应的操作语义。新的语言兼顾了实用性和表达能力,可使编程人员表达出其想要的一致性语义,从而避免(1)因为遗漏重要的一致性约束而导致的错误;和(2)由于引人不必要的一致性约束所产生的程序效率损失。其次,本文给出了细粒度一致性模型的相关性质,便于编程人员对其有更深刻的理解。而后,本文给出用于验证程序满足收敛性和特定不变量的程序逻辑,并给出了程序逻辑的可靠性证明。相关证明的关键引理已在定理证明工具Coq中实现,共计约3100行。最后,本文给出了基于上述一致性模型和语言的分布式备份系统设计和实现。系统使用Java语言实现,共计约5300行代码。除此之外,为保证系统正确性,我们使用了 TLA+模型检查工具对其进行了死锁和活性检查,共计约1500行代码。最后,我们利用该语言实现3个应用程序,并在不同工作负载下进行对比实验。实验结果表明了语言的通用性和系统的可扩展性。