Source-linked AI summary
Certified Compilation in the TELEPERM XS Nuclear Safety I&C Platform
Alexandre Berard, Richard B. Kreckel
TL;DR
Nuclear safety toolchains must verify generated code and show that translation preserves semantics, yet recurring structure-copy patterns in TXS Core’s generated code perform poorly. The paper improves the compiler and code generator using formally supported transformations, reducing code size and runtime while also reducing the compiler’s trusted computing base.
Problem
Recurring structure-copy patterns in TXS Core’s generated code compile poorly, while nuclear safety toolchains must provide evidence that translation preserves semantics.
Source: §1 · p. 2, §3.1 · pp. 5–6Method
The paper improves CompCert’s handling of memory copies with verified transformations and adjusts TXS Core code generation to create more mergeable copies.
Source: §3.3.1 · p. 7, §3.3.2 · p. 8, §3.3.4 · p. 9Results
16% on average additional improvement comes from sorting generated variables, effective only together with the compiler improvement; the resulting code is much smaller and faster and reduces the compiler’s TCB.
Source: §3.4 · p. 10, §5 · p. 11Takeaways & Limitations
Reducing the compiler’s TCB directly improves the safety case, while increased toolchain trust can support later local functional changes to FBDs without replacing test-bay V&V.
Source: §5 · p. 11CompCert’s correctness proof remains limited by its trusted computing base, and TXS Core avoids unproven compiler extensions.
Source: §2.3 · p. 5
Abstract
from arXiv · showhide
The large safety instrumentation & control (I&C) systems in civil nuclear power plants (NPPs) are mainly safe-shutdown systems (reactor protection) or limitation and control systems. Framatome's established TELEPERM XS (TXS Core) product family is a digital I&C system platform to cover all these applications. We illustrate the role of verification in the different stages of the software production toolchain, focus on the formal compilation process, and discuss the contribution of the CompCert certified compiler to the safety case of the product. Scrutinizing the object code produced by this compiler has exhibited suboptimal run-time performance in a certain simple but recurring generated code pattern. We explain how formal methods allow us to address this issue in the compiler while simultaneously reducing its trusted computing base (TCB), thereby strengthening the safety case rather than merely preserving it.
1 Introduction
Nuclear safety I&C software faces strict requirements for development and verification, while function block diagrams remain a prevailing programming approach. The paper examines verification across the TXS Core toolchain, focusing on certified compilation and a recurring generated-code performance weakness.
1 Introduction
- FBDs remain prevalent for reactor protection, limitation, and control, while their dataflow structure suits process-centric requirements and control engineers.Pre-developed, qualified function-block libraries also reduce low-level programming for control engineers.Source: §1 · p. 1
- Nuclear safety I&C toolchains must produce output that is comprehensively verified and provide evidence that translation preserves input semantics.IEC 60880 requires mitigation against errors potentially introduced by translation tools.Source: §1 · p. 2
- The paper presents TXS Core’s verified code generation and certified compilation, then addresses recurring generated-code patterns through compiler and code-generator changes.It also places the work in the safety case.Source: §1 · p. 2
2 The TXS Core Fully Verified Toolchain
TXS Core converts graphical FBDs into certified binaries through automated stages. An independent verifier checks the FBD-to-C translation, and CompCert formally proves semantic preservation during compilation.
2 The TXS Core Fully Verified Toolchain
- The toolchain starts with engineers assembling FBDs from qualified function blocks, then translates them into certified binaries through fully automated stages.The verifier runs before compilation is invoked.Source: §2 · p. 3, §2.2 · p. 4
2.1 Code Generation
- TXS Core’s graphical FBDs become ISO C containing qualified function-block calls and dataflow glue code, and the automated stages require no user intervention.The generated C is often long but linearly structured.Source: §2.1 · p. 3, §2 · p. 3
2.2 Automated Code Verification
- The independent verifier establishes semantic preservation by checking that generated structures match the FBD and code respects its implicit causal relations.For each signal, source function blocks must be called before destination blocks; this causality check is necessary and sufficient for preservation.Source: §2.2 · p. 4
2.3 Certified Compilation
- CompCert compiles generated ISO C to ArmV7 object code, with its optimizing transformations formally proven to preserve semantics and checked by Rocq at each build.Within TXS Core, unproven CompCert extensions are strictly avoided; the proof remains limited by its trusted computing base.Source: §2.3 · pp. 4–5
3 COMPCERT Improvements
CompCert’s optimization set lacks some state-of-the-art algorithms, while adding optimizations requires substantial proof work and may require changes to its theory models. CHAMOIS-CompCert provides more aggressive optimizations and a framework for developing them.
3 COMPCERT Improvements
- CompCert lacks some state-of-the-art optimization algorithms, whose addition requires semantic-preservation proofs and may require changes to its theory models.The compiler already includes dead-code elimination and constant propagation.Source: §3 · p. 5
- CHAMOIS-CompCert, a frequently updated fork, adds more aggressive optimizations and a framework that facilitates writing them.The paper describes its recent improvements as addressing cases where both CompCert and the fork fail to optimize TXS Core’s generated C.Source: §3 · p. 5
3.1 Suboptimal Patterns Identified in Generated Code
Generated FBD code contains repetitive assignments for routing I/O signals, and small signal structures turn these into costly structure copies. CompCert’s treatment of these copies leaves the pattern poorly optimized and relies on unverified backend expansion code.
3.1 Suboptimal Patterns Identified in Generated Code
- Repeated I/O-routing assignments become heavy structure copies because each signal is represented as a small C structure.The patterns occur around FDGIN and FDGOUT functions.Source: §3.1 · p. 5
- CompCert propagates structure-copy Memcpy built-ins through its intermediate representations, leaving them insensitive to optimization and poorly compiled.Their assembly expansion is performed by unverified OCaml code in the compiler’s TCB.Source: §3.1 · pp. 5–6
3.2 Overview of CHAMOIS-COMPCERT’s Formal Verification Framework
CHAMOIS-COMPCERT combines symbolic execution with formally verified framework components to validate optimization transformations in BTL and the backend.
3.2 Overview of CHAMOIS-COMPCERT’s Formal Verification Framework
- A BTL symbolic execution engine verifies middle-end optimization oracles by defensively validating proposed code transformations.The engine is part of CHAMOIS-COMPCERT’s block-verification framework.Source: §3.2 · p. 6
- The formally verified framework supplies oracle-computed information that lets the checker validate rewrites using invariants and pointer nonaliasing.This supports simplification across blocks and permutation of load and store instructions.Source: §3.2 · p. 6
- A separate backend symbolic engine validates instruction scheduling and peephole mutations on an abstract representation of target-specific assembly operations.The paper reports porting the postpass scheduling algorithm to the ArmV7 backend.Source: §3.2 · p. 6
3.3 Improvements Made to Compiler Built-in Memory Copies
The section improves COMPCERT’s handling of built-in memory copies through verified merging, realignment, and expansion, replacing complex unverified lowering with a simpler translation and reporting speedups on TXS hardware.
3.3 Improvements Made to Compiler Built-in Memory Copies
- COMPCERT represents Memcpy as contiguous-byte loads from a source followed by stores to a destination, parameterized by copy size and alignment.The proposed improvements exploit statically known structure-field offsets and global memory-block alignment to merge adjacent copies and choose wider instructions.Source: §3.3 · p. 6
3.3.1 Merging memory copies with a verified oracle
- A greedy BTL-stage oracle merges copies only when source and destination blocks are contiguous, while symbolic checking validates transformations and memory-operation reordering.The checker receives original-copy annotations to validate address ranges and writing modes; overlapping cases remain unsupported by the current oracle.Source: §3.3.1 · pp. 6–7
3.3.2 Realignment analysis
- Realignment analysis tracks the maximal achievable alignment α and offset o, enabling wider fragments across merged structures and reducing the number of expanded load and store instructions.The global memory-block alignment β and source and destination offsets inform the computed pair (o, α).Source: §3.3.2 · p. 8
3.3.3 Formal expansion of memory copies with fragmentation
- A proven local-simulation pass expands Memcpy into atomic operations arranged as a prologue, repeated aligned copy part, and epilogue.Large repeated copy parts may use a loop; the proof preserves execution state apart from fresh values introduced during expansion.Source: §3.3.3 · p. 8
- Btlmemcpy speeds FDGIN functions by a factor of 1.64 on average; variable sorting adds a factor of 1.16, for a total average speedup of 1.90.The figure reports measurements across 82 TXS CPUs.Source: Figure 5 · p. 9
3.3.4 Reduction of COMPCERT’s Trusted Computing Base
- Atomic-copy normalization removes the complex, unsafe general-case Memcpy translation from COMPCERT’s TCB and replaces it with a simpler one-to-one translation.The translation cannot be removed entirely because Memcpy pointer fragments carry semantics that cannot be bound to a valid byte type.Source: §3.3.4 · p. 9
3.4 Evaluation Within the TXS Core Toolchain
An experiment on real TXS Core hardware found that compiler improvements speed up generated-code patterns, while sorting computed signals adds an average gain only in combination with those improvements.
3.4 Evaluation Within the TXS Core Toolchain
- The CHAMOIS-COMPCERT improvements significantly speed up the generated-code patterns observed in FDGIN functions.The evaluation describes these as recurring patterns in generated code.Source: §3.4 · p. 10
- Variable sorting adds an average 16% improvement, but only together with the compiler improvement.The evaluation used an actual TXS Core safety I&C specification on real TXS Core hardware.Source: §3.4 · pp. 9–10
4 Related Work
Related work covers diverse back translation of generated code and formally verified compilation, while the paper identifies memory-copy merging for generated PLC code as a novel optimization pattern.
Related work
- RETRANS semi-automates diverse back translation of TXS Core C code, while the TXS Core verifier is presented as a fully automated, complete, and direct nuclear-industry tool.The verifier checks the <FB relation for all netlist edges, addressing the reliance of RETRANS and GET-R1 on sequentialization hints that are not part of the original specification.Source: §4 · p. 10
- Vélus compiles Lustre to CompCert Clight, but is not described as integrated into tooling suitable for graphical FBDs under nuclear-industry standards.Lee et al. translated FBDs to Verilog to check equivalence with target C before compilation; CompCert use in nuclear safety has also involved additional checks of linked executables or ELF objects,,.Source: §4 · p. 10
- Memory-copy merging for generated embedded-PLC code is presented as novel, and its recurring structures and assignments appear to have escaped popular benchmarks.Prior optimization work includes wide-register copying and merging adjacent 4-byte copies into one 8-byte copy in unverified compilers such as GCC and Clang.Source: §4 · p. 10
5 Conclusion and Outlook
The work improves CompCert-generated code while reducing the compiler’s TCB, strengthening the safety case. These formal assurances do not replace comprehensive I&C validation, and practical and administrative work remains for adoption.
Conclusion and outlook
- Formal verification that FBD-to-executable translation preserves semantics does not replace comprehensive I&C system validation.The authors note that toolchain trust is unlikely to obsolete test-bay V&V.Source: §5 · p. 11
- The CompCert improvement yields code that is smaller and faster while reducing the compiler’s TCB, directly improving the safety case.Greater trust in the toolchain can support later local functional changes to FBDs, although it is unlikely to eliminate test-bay V&V.Source: §5 · p. 11
- Practical and administrative activities remain before the CompCert improvements can be introduced into the TXS Core toolchain.Source: §5 · p. 11