RISC-V bugs found by Princeton


Princeton TriCheck r Margaret Martonosi (centre) Yatin Manerkar Caroline Trippel

They were testing a technique created for analysing memory use, and found over 100 errors involving incorrect orderings in the storage and retrieval of information from memory in variations of the RISC-V processor architecture.

Called TriCheck, its name is derived from three general levels of computing: the high-level programs, the instruction set architecture, and the underlying hardware implementation.It ensures memory-ordering guarantees made by these three levels are aligned.

“Incorrect memory access orderings can result in software performing calculations using the wrong values,” said Princeton Professor Margaret Martonosi, who heads the TriCheck team. “These in turn can lead to hard-to-debug software errors that either cause the software to crash or to be vulnerable to security exploits.”

According to Princeton, the RISC-V Foundation said that the errors would not affect most versions of RISC-V but would have caused problems for higher-performance systems.

RISC-V Foundation chair Krste Asanović said that the Foundation has formed a working group to solve the memory-ordering problems, headed by former Martonosi student Daniel Lustig, now at Nvidia.

Lustig said work is underway to improve the RISC-V memory model. “RISC-V is in the fortunate position of being able to look back on decades’ worth of industry and academic experience. It will be able to learn from all of the insights and mistakes made by previous attempts.”

Asanović, a professor at University of California-Berkeley, said the RISC-V project was looking for input from the design community to “fill the gaps and the holes and getting a spec that everyone can agree on”, adding: “The goal is to ratify the spec in 2017. The memory model is part of that.”

The RISC-V project essentially offers the ‘instruction set architecture’ – the list of instructions – around which processor designers would construct the hardware and app writers would weave software.

RISC-V was initially developed at Berkeley, and is now run by the Foundation, whose members include Google, IBM, Microsoft, NVIDIA and Oracle, as well as universities and other organisations.

The work was presented as ‘TriCheck: Memory model verification at the trisection of software, hardware, and ISA‘ at the ACM International Conference on Architectural Support for Programming Languages and Operating Systems this week. This detailed paper also discusses a known ARM memory issues and its official work-around.

The authors ran tests of the RISC-V instruction set using a high-level program written in C. On one particular RISC-V-compliant design, TriCheck found 144 errant programs out of 1,701 test programs.

These memory issues arise when concurrent operations are performed on the same regions of memory. “It puts a heavy demand on the computer’s ability to interleave and properly order memory usage.” said Princeton.

Subtle changes in the machine level, the compiler or a high-level programming language can have unintended effects.

“If I write a program in C, it makes some assumptions about memory ordering,” said Martonosi. “Subsequently, a different set of memory ordering rules are defined by the instruction-set architecture. We need to check that the high-level program’s assumptions are accurately supported by the underlying instruction set and processor design.”

TriCheck, which has taken four years to develop, uses formal specifications of memory ordering – axioms.

For a given program, compiler, instruction set and hardware implementation, TriCheck can enumerate many ordering possibilities from these axioms, and then check for errors. By expressing memory-ordering possibilities as connected graphs, it can identify potential errors by looking for cycles in the graphs.

Photo: Professor Margaret Martonosi (centre) with fellow TriCheck researchers Yatin Manerkar and Caroline Trippel
(by David Kelly Crow)



Source link

Leave a Reply

Your email address will not be published. Required fields are marked *