New programming language and tool ensures code will compute as intended

Not long ago, people using Microsoft Word would check for spelling errors by specifically telling the software to run "Spell Check." The check took a few seconds to do, and users could then go in and fix their typos. Nowadays, Spell Check runs automatically as users write—as I write this story.

Microsoft Word and its constant running of Spell Check is a basic example of "concurrent" programming—a form of computing in which an executable runs simultaneously with other programs and computations. Most programs today are concurrent programs, ranging from your operating system to the many applications, from word processing to web browsing, that people use on a daily basis.

"When you have multiple things happening at the same time, you need some way of coordinating between them to make sure they're not stomping on each other," says CyLab's Bryan Parno, an associate professor in Electrical and Computer Engineering and the Computer Science Department. "Historically, this has been a very buggy process."

Parno and a team of researchers recently published a new coding language and tool for high-performance concurrent programs that ensures that programs are provably-correct—that is, that the code is mathematically proven to compute correctly. The language and tool, named Armada, was presented at this year's Conference on Programming Language Design and Implementation, and the paper received a Distinguished Paper award.

"What's novel about Armada is that it's designed to be extremely flexible so you can write the code the way you want so it'll go as fast as it can," says Parno. "But you'll still get strong assurance that it's going to do the right thing and not mess anything up on the back end."