Freeman's Blog

一个菜鸡心血来潮搭建的个人博客

0%

项目

发表于 更新于 分类于

TLA+ ToolBox

项目总述

  • TLA+：TLA意为行为时序逻辑，TLA+则是一种形式化语言，以行为时序逻辑的方式对软件程序、算法或者协议进行高层次的建模，描述系统的行为，帮助开发人员对程序和算法有更清楚的认识，在系统设计阶段避免一些可能出现的错误。（对代码进行测试是一种发现编码错误的手段，但不是一种高效的对系统设计进行检查的手段）
  • TLA+的做法是使用基于状态的方式来描述系统的行为。用对所有状态变量的一次赋值来表示一个系统的全局状态。用状态转移前后状态变量的关系来表现所有可能出现的状态变化。于是系统的可能行为集合就可以被分为两个部分：所有可能的初始状态和所有可能的状态转移方式。
  • TLA+ Toolbox是形式化语言TLA+的集成开发环境，其中包括了模型检查器TLC。用户使用TLA+对系统建立的模型包括了系统的初始状态和所有可能的状态转换，实际上建立了整个系统的状态图。模型检查器TLC可以遍历用户系统对应的状态图，检查每个状态是否能够满足用户定义的一些约束，以此来帮助用户发现系统模型的潜在问题。
  • 个人负责的工作：提供TLC的运行时API，用户使用这些API可以在TLC运行时获取他们关心的一些状态信息，例如当前已经检查的模型深度和当前正在检查的状态。用户还可以使用这些API对运行中的TLC进行一些操作，例如让计算任务暂停，为当前任务创建检查点以便恢复执行等。这些API计划使用JMX进行提供。同时开发云计算功能模块：用户提供云服务提供商的token，TLC可以自动地使用云服务提供商的SDK创建云实例，将TLC主程序和用户编写的模型打包上传到云实例，在云实例上执行计算任务，并在计算任务完成时自动给用户发送邮件并关闭云实例。

实际应用场景

  • …

TLA+可以举个例子吗

  • TLA+ 比较常用的地方是用于精确地对并发系统或分布式算法进行建模

    2PC协议的TLA实现

JMX？

  • 定义符合JMX规范的Java对象MBean，将其注册到Java内置的MBean服务器中让MBean服务器对其进行管理，即可暴露一些当前应用的运行时信息，提供一些可读写的字段，提供一些可以在运行时执行的操作。
  • 定义MBean一般是先定义一个XXXMBean接口，在接口中说明所有可以访问的属性和所有可以执行的方法，然后定义XXXMBean的实现类XXX，在实现类中提供实际的数据访问、执行实际的操作。
  • MBean的名称规范(ObjectName): 至少要包括一个域(domain)和一系列的键值对。Domain一般可以使用包名。
  • MXBean: 只会包含预定义的数据类型，因此任何客户端（包括远程客户端）都可以使用，而不需要引用特定的自定义类型。MXBean接口不要求实现类名与接口名有对应关系。
  • 如果要在MXBean里使用复杂类型，复杂类型的数据会被映射为简单类型。

项目实现细节

模型检查器的基本原理

  • 本质上，用户所编写的模型规定了系统的初始状态和所有可能的状态转换，相当于定义了一个状态图。模型检查器的原理大致是对这个状态图进行广度优先遍历，并检查每个状态是否出现不满足Safety属性。为了实现广度优先遍历，TLC需要维护2个数据结构：一个记录所有已经检查过的状态的集合，一个用于实现广度优先遍历的队列。TLC可以开启多个worker线程，worker线程对已检查过的状态集和状态队列的独写使用ReadWriteLock来保证线程安全。
  • 系统的一次完整执行称为一次系统的行为。而系统的一次完整执行通常是可以用一个条件来定义的（某些事情总要发生，Liveness属性）。如果一个执行trace一次都没有触发过termination，说明检查到了违反liveness属性的执行序列。

集合怎么实现?

队列怎么实现?

  • 队列实现为一个硬盘上的文件，开头和结尾保留一定量的元素在内存中。使用了专有的线程对队列开头和结尾的缓冲区进行预载。

提供什么运行时API?

  • 启动与暂停：
    • 暂停：设置队列的标志变量stop，worker线程调用入队列或出队列的方法使用synchornized关键字修饰，调用时必须检查标志变量的值，如果发现stop = true则会调用wait方法让自己挂起。
    • 重启：修改stop为false，并且调用notifyAll唤醒所有在队列上等待的线程
  • 单步调试：
    • 使用模型检查器的内部类解析用户编写的模型，生成所有的初始状态，让用户自行挑选下一状态并单步观察状态的变化。

云计算模块的基本原理

  • 让用户选择云服务的提供商并设置必要的认证凭据（ID, SECRET），云计算模块负责自动创建特定规格的实例，并通过SSH连接到云实例上，完成云实例的准备并下载运行所需要的依赖（例如JDK）。同时云计算模块会负责将用户在本地创建的模型文件与模型检查器的可执行jar文件打包上传到云实例上。模型检查器执行完毕后首先将执行结果的输出文件使用邮件发送到用户提供的邮件地址。
  • 主要负责为该模块添加阿里云支持，项目原本使用了jclouds屏蔽不同云服务提供商的接口差异，但是jclouds并未在正式版中提供阿里云支持，因此计划是尝试将阿里云的SDK进行包装和适配，尽可能地复用原有的代码。
  • 怎么发送邮件
    • 让用户提供邮件地址，可以通过邮件地址的@后的域名查询邮件地址对应的SMTP服务器域名。DNS服务器会返回对应的MX记录
    • 至于怎么知道哪台服务器才存放这个MX记录，我觉得只需要和查找A记录一样，先找到@后的域名所在的服务器就可以找到对应的MX记录了。
    • 或者可以使用阿里云的邮件推送服务
  • JVM调优：-XX:+UseParallelGC，使用