This paper reports our experience in modeling Raft in the LNT process algebra. We found a couple of issues with the original TLA+ specification of Raft, which has been corrected since. More generally, this exercise offers a great opportunity to discuss how to best use the features of the LNT formal language and the associated CADP verification toolbox to model distributed protocols, including network and server failures.
Новость одной строкой: вышла новая версия стандарта OpenCL 3.0 для параллельных вычислений на разных мультиядерных устройствах. В отличие от nVidia CUDA, которая работает только на GPU nVidia, OpenCL может использоваться на GPU от AMD и nVidia + на многоядерных CPU (то есть вообще на всех современных процессорах, даже ARM).
В тему OpenCL и CUDA – буквально вчера увидел такую надстройку над ними – https://www.khronos.org/registry/SYCL/specs/sycl-1.2.1.pdf Идея в том, чтобы к OpenCL (в первую очередь) добавить фишек C++11 и выше. Ну и пероложить максимум boilerplate на компилятор (где это и должно быть)
Уже есть реализация спеки – https://software.intel.com/en-us/oneapi/dpc-compiler В описании они называют приложения CUDA – легаси)) Includes a compiler to deploy across diverse hardware targets and a compatibility tool for migrating legacy CUDA* applications to a multiplatform program in DPC++.
Единственное, пока не нашёл реализацию именно для GPGPU nVidia, но тем не менее, есть для CPU/GPU Intel + заявляется поддержка OpenCL AMD, а значит скорее всего будет работать на радеонах.