#prog #cpp #article
Валидатор (и папир о нём) компиляций, проводимых LLVM, по отношению к многопоточным программам. Поспособствовал выявлению нескольких багов в LLVM.
"We construct a validator that checks whether the transformations performed by LLVM are correct according to the C11 memory model or our inferred LLVM memory model. The validator takes as inputs the programs before and after a set of transformations. It compares them by matching their memory access patterns and reports on whether it could find a matching demonstrating that transformation is correct."
Анализатор, к сожалению, не вполне справляется с циклами и использует для них эвристику, которая может поймать только неправильную компиляцию между первыми двумя итерациями цикла. Это вполне объяснимо, поскольку частью анализа является сопоставление потока исполнения программы до и после трансформаций, а эта задача с введением циклов резко усложняется. Для программ же без циклов проводимый анализ точен и корректен (sound).
Надо отметить, что модель памяти, подразумеваемая LLVM, менее строгая, чем модель памяти C11, поскольку допускает добавление спекулятивных доступов к значениям. В связи с этим валидатор может работать, проверяю корректность трансформаций на основе обоих моделей.
Валидатор (и папир о нём) компиляций, проводимых LLVM, по отношению к многопоточным программам. Поспособствовал выявлению нескольких багов в LLVM.
"We construct a validator that checks whether the transformations performed by LLVM are correct according to the C11 memory model or our inferred LLVM memory model. The validator takes as inputs the programs before and after a set of transformations. It compares them by matching their memory access patterns and reports on whether it could find a matching demonstrating that transformation is correct."
Анализатор, к сожалению, не вполне справляется с циклами и использует для них эвристику, которая может поймать только неправильную компиляцию между первыми двумя итерациями цикла. Это вполне объяснимо, поскольку частью анализа является сопоставление потока исполнения программы до и после трансформаций, а эта задача с введением циклов резко усложняется. Для программ же без циклов проводимый анализ точен и корректен (sound).
Надо отметить, что модель памяти, подразумеваемая LLVM, менее строгая, чем модель памяти C11, поскольку допускает добавление спекулятивных доступов к значениям. В связи с этим валидатор может работать, проверяю корректность трансформаций на основе обоих моделей.
