无服务器计算的形式化基础

论文地址： 无服务器计算的形式化基础JangDA等人，OOPSLA ‘19

Jangda等人。今年在OOPSLA获得了一个杰出的论文奖，他们的研究成果是“无服务器计算的正式基础”。论文的中心是他们观察到无服务器的执行环境有许多独特的特性（例如，启动环境的热启动/重用），这使得构建正确的环境变得更加困难。应用。它们显示了无服务器函数可以安全地忽略这些特性的条件，从而变得更容易推理。他们还介绍了一种基于箭头的函数合成语言。

无服务器时需要注意的事项
无服务器计算抽象尽管有许多优点，但它暴露了一些低级操作细节，使得程序员很难编写代码并对代码进行推理。例如，为了减少延迟，无服务器平台尝试重用同一个函数实例来处理多个请求。但是，这种行为是不透明的，很容易编写一个无服务器的函数，在重用时产生不正确的结果或泄漏机密数据。一个相关的问题是，无服务器平台在空闲时会突然终止函数实例…

• 这些第一个问题与无服务器环境中的误用/误解状态有关。无服务器函数是无状态的，但可以在调用之间机会性地重用缓存状态，以加快启动时间。

论文中“这样做是错误的”的例子有一个代码示例，其实质如下：

好吧，是的——如果你想让“持久”状态保持在一个没有服务器的函数中，那就不太好了！别那么做！更可能落入陷阱的是缓存某些状态以便在函数执行过程中机会性地重用，但如果该状态绑定到给定用户，则根本无法保证下一次执行将针对同一用户。

• 第二个考虑是一个函数的许多实例可以并行执行（这不是重点吗？！）。没有函数关联的概念，因此来自同一源的请求也可以由不同的函数实例处理。因此，您可能需要在函数执行环境之外的共享状态的协调机制（例如，具有事务支持的持久存储）。

到目前为止，我觉得这有点像是无事生非，但第三个考虑肯定会更棘手，以获得正确。它涉及到给定至少一次执行语义的对幂等性的需求（即，事件可能会被重试，这取决于您配置重试策略的方式）。
大多数平台在响应单个事件时至少运行一次函数，这在函数有副作用时可能导致问题。

如果您的函数不是自然的等幂函数，则可能需要使用一些策略，例如记住以前看到的事件id。作者在这里没有提到的是，只有当非幂等性涉及到事务性资源管理器执行的操作（您也在使用事务性资源管理器来存储已处理的事件id）时，这才真正起作用。如果副作用是发送电子邮件，祝你好运！

Lambda操作语义
\lambda{\mathbb{\lambda}是一种操作语义，它捕获了无服务器平台的这些微妙之处。无服务器函数本身由三个函数定义：

• init定义初始状态
• recv定义了在收到请求时的行为，并且
• step定义了一个由函数执行的处理步骤，该函数可以生成一个命令t，供无服务器平台执行。在我们的旅程中，此时唯一有效的命令是返回。

无服务器平台本身由正在运行或空闲的函数实例、挂起的请求和响应的集合组成。

关联语义由六个规则组成：

• REQ为每个请求分配一个全局唯一标识符
• 在稍后的某个时间，平台可能会执行关联函数的新实例的冷启动
• 或者它可以选择重用现有的空闲（WARM）函数实例
• 函数所采取的内部步骤是隐藏的
• 生成返回命令的函数步骤将导致发送响应并将函数实例标记为空闲
• 函数实例（不管是否空闲）随时可能在没有警告的情况下消亡

注意：

• 实例启动是不可见
• 状态在热启动期间重复使用
• 函数实例终止不可见
• 函数实例可以随时开始处理挂起的请求，即使现有函数正在处理该请求
• 每个请求最多从一个函数实例接收一个响应，处理同一请求的其他实例最终会卡住并终止。

一个原始的语义，当它可以安全的被使用
考虑到在这样一个环境中编程的微妙之处，作者问是否有一种方法可以简化事情…
首先，我们定义了一个更简单的无服务器计算的朴素语义，它消除了\lambda{\mathbb{\lambda}的大多数非直观行为。其次，利用弱互模拟定理，我们精确地刻画了当原始语义和lambda{\mathbb{\lambda}重合时的特征。这个定理一劳永逸地解决了无服务器执行的低级细节问题，从而允许程序员使用简单的语义进行推理，即使他们的代码运行在一个成熟的无服务器平台上。
在原始的语义中，平台一次对一个请求运行一个函数f，抽象出并发执行和热启动的细节。程序员可以在这个更简单的世界中推理，如果他们可以将安全关系定义为程序状态上的等价关系，这样：
无服务器函数在其输出中是确定的：它在任何等价状态下生成相同的可观察命令（如果有的话）所有最终状态都等同于初始状态
请注意，一个简单的状态可能等同于多个不同的\lambda{\mathbb{\lambda}状态，反之亦然。考虑到上述条件，本文第4节中的弱互模拟定理允许程序员合理地忽略平台的底层细节。
不过，有些微妙之处已经简单地转移到定义等价关系上了！例如，我最初认为规则2的含义是，在每次执行结束时，必须消除所有的瞬态（这消除了热启动和冷启动之间的差异，但并不十分有用）。但实际上，这一切都归结于如何定义关系：即使缓存状态不同，也可以将两个程序状态指定为等效。

外部服务该如何对接
功能本身并不是非常令人兴奋——要在现实世界中完成任务，它们通常需要与外部服务交互。
不幸的是，完全由程序员来确保他们的代码是幂等的，并且平台没有提供关于等幂意味着什么的明确解释，因为无服务器函数执行热启动、执行并发，并且可能在任何时候失败。
第5节将事务语义添加到假设键值存储的模型中。语义允许使用这种存储的函数成为等幂函数，前提是它们在事务更新中将每个输出值保存到由请求id键控的存储中。具有相同请求id的任何后续请求都应获取存储中保存的值。实际部署至少必须处理请求结果的某些到期机制，这样状态就不会无限增长。
再一次，这只涵盖了所有“副作用”实际写入键值存储的情况。任何与其他服务的交互，或任何其他可观察到的副作用，而你又得靠自己了。

SPL，一种无服务器的组合语言
本文的最后一部分介绍了SPL，一种用于函数组合的“无服务器编程语言”（c.f.AWS Step函数，或OpenWhisk导体）。SPL基于Hughes的Arrows，支持三个基本的arrow组合器：

调用无服务器函数

• 按顺序运行两个子程序
• 在元组的第一个组件上运行一个子程序，并在未更改的情况下返回第二个组件。
• 这三个操作足以描述无服务器函数的无循环和无分支组合。添加对有界循环和分支的支持很简单…

直接使用箭头组合符表示的SPL程序很难让程序员理解，因此可以使用基于Paterson箭头符号的表面语法，看起来有点像这样：

我们已经构建了一个SPL的可移植实现（1156 LOC of Rust），它可以调用公共云中的无服务器功能……这个可移植实现帮助我们确保SPL的设计独立于Open Whisk的设计和实现，我们已经使用它来探索无服务器平台可能希望提供的其他类型的功能。
SPL在这里得到了一件好事（比如AWS Lambda/Step函数在imho中出错了！）是组成属性。因此，构建高阶SPL程序很简单。例如，在AWS上，当lambda变得有点太大，并且您希望将其演变为一个step函数时，就需要做太多的更改。