新的编程语言和工具可确保代码按预期进行计算

不久之前，使用Microsoft Word的人会通过明确告诉该软件运行“拼写检查”来检查拼写错误。这项检查花费了几秒钟的时间，然后用户可以进入并解决他们的错字。如今，我撰写此故事时，拼写检查会随着用户的书写自动运行。

Microsoft Word及其不断运行的Spell Check是“并发”编程的基本示例，这是一种计算形式，其中可执行文件与其他程序和计算同时运行。当今，大多数程序都是并发程序，从您的操作系统到许多应用程序，从人们每天使用的文字处理到Web浏览，不一而足。

CyLab的电气与计算机工程与计算机科学系副教授Bryan Parno表示：“当您同时发生多件事情时，您需要某种协调方式，以确保它们之间不会互相踩踏。”部。“从历史上看，这是一个非常麻烦的过程。”

Parno和一组研究人员最近发布了一种用于高性能并发程序的新编码语言和工具，可确保程序可证明是正确的，也就是说，该代码在数学上被证明可以正确计算。在今年的编程语言设计与实现会议上介绍了名为Armada的语言和工具，该论文获得了杰出论文奖。

“关于Armada的新颖之处在于它的设计非常灵活，因此您可以按照自己的方式编写代码，从而使其能够尽快运行，” Parno说。“但是您仍将获得有力的保证，它将做正确的事情，并且不会弄乱后端的任何事情。”

帕诺(Parno)将并发程序的复杂性及其对错误的敏感性比作拍卖。通常，一个拍卖师会收到很多人的出价。如此之多的人和一位拍卖师，可能需要很长时间才能达到最高出价。如果将每个人分成十个房间，每个房间都有自己的拍卖师，那将会加快速度，但是拍卖师很难保持协调。会有很多错误的余地。

帕尔诺说：“所有拍卖商都必须有一种相互交流的方式，同时努力争取所有房间的最高出价。” “这可能会变得非常复杂，这就是为什么您通常不会看到以这种方式进行拍卖的原因。”

帕尔诺认为，舰队将使编写并发程序的任何人受益，这些并发程序涵盖了广泛的应用程序。

“从薪资系统到医院记录再到任何形式的电子商务，它们都由数据库支持，而数据库始终将由并发软件支持，” Parno说。“除了简单的程序，如今，几乎所有内容都具有某种并发性。”