Computer scientist Andrew Reynolds develops logic solvers that use automatic reasoning to test things like hardware and software design. When the time comes to make a modification, he needs to verify that he didn’t introduce any bugs, and that the tools run as fast as they did before.
For the past five years, a University of Iowa high-performance computing cluster called StarExec has provided daily reassurance that the software he’s developing is performing optimally.
“We need to do a lot of testing, even with minor daily changes, to make sure we didn’t break anything,” says Reynolds, assistant research scientist in the Department of Computer Science. “StarExec has the computing power to give me reassurance.”
StarExec harnesses the power of 200 computers to facilitate experimental evaluation of logic solvers, broadly understood as automated tools based on formal reasoning.
As a free, public service, it provides a single piece of storage and computing infrastructure to logic-solving communities and their members. It reduces duplication of effort and resources and enables individual researchers or groups who would otherwise not have access to comparable infrastructure.
StarExec is heavily utilized, tackling more than a million logic problems every week. Fourteen computer science research subcommunities around the globe use the resource, and it’s the go-to host for logic-solver competitions.
Since 2013, the National Science Foundation has supported the project through a Computing Research Infrastructure Grant—initially a $100,000 planning grant, followed by $1.7 million, and recently another $500,000 to add more computing power and storage. Its name reflects its versatility—a star in computer science stands for “anything,” and exec is short for “execute.”
“It’s an effective solution that a lot of researchers needed—any community can execute logic solvers on StarExec,” says Aaron Stump, professor of Computer Science and co-principal investigator of the grant, with fellow UI Computer Science Professor Cesare Tinelli and Geoff Sutcliffe of the University of Miami. “This is meant to be the one infrastructure to serve everyone’s needs. That vision has, after quite a bit of work, been completely realized.”
The Olympics of logic solving
StarExec has become a popular platform for logic-solving competitions, where computer scientists see how their code performs against challengers to solve as many problems as possible in a specific time. The matches are important to logic-solving communities because they help spur advances in methods.
It has hosted 38 competitions over the years, and this past summer had a breakout year, hosting nine of 13 competitions in the FLoC Olympic Games, the most illustrious contest in the field.
“We are the world’s infrastructure for running logic-solving competitions,” Stump says. “Virtually every competition we know is using this service. To that extent, I would say it succeeded beyond our dreams.”
A training ground for students
Stump notes that StarExec wouldn’t be what it is without the people behind it. The Linux team in College of Liberal Arts and Sciences Technology Services supports the system, and UI students have been instrumental in its success, contributing to its 100,000 lines of code in a host of different languages.
“A lot of Star Exec alums have commented when they went on to jobs in the field that this was a standout coding experience,” Stump says. “It’s rare for undergrads to be able to work on something this complicated on a live system; it feels much more real than a lot of the work they do in class. Those who have worked on this project experienced a lot of development in coding and debugging skills.”