# Cooling and Timing Tests of the ATLAS Fast Tracker VME boards

S. Sottocornola, A. Annovi, N.V. Biesuz, E. Brost, M. Calvetti, C. Gentsos, T.
Holmes, L. Horyn, T. Iizawa, A. Lanza, J.D. Long, P. Mastrandrea, I. Maznas,
A. Negri, D. Calabro, M. Piendibene, C. Roda, E. Romano, T. Seiss S.
Sottocornola, A. Lanza, A. Negri, D. Calabro, E. Romano are with Sezione di
Pavia INFN, via Bassi 6, Pavia, Italy (email: simone.sottocornola@cern.ch). A.
Annovi, N. V. Biesuz, P. Mastrandrea, M. Calvetti, M. Piendibene and C. Roda
are with the University of Pisa and INFN Sezione di Pisa. E. Brost is with
Brookhaven National Lab. C. Gentsos is with CERN. T. Holmes, L. Horyn, T.
Seiss are with University of Chicago. J. D. Long is with University of
Illinois Urbana-Champaign. T.Iizawa is with University of Geneva. I. Maznas is
with Aristotle University of Thessaloniki.

###### Abstract

††Copyright 2020 CERN for the benefit of the ATLAS Collaboration. CC-BY-4.0
license.

The Fast Tracker (FTK) is an ATLAS trigger upgrade built for full event, low-
latency, high-rate tracking. The FTK core, made of 9U VME boards, performs the
most demanding computational task. The Associative Memory Board Serial Link
Processor (AMB) and the Auxiliary card (AUX), plugged on the front and back
sides of the same VME slot, constitute the Processing Unit (PU), which finds
tracks using hits from 8 layers of the inner detector. The PU works in
pipeline with the Second Stage Board (SSB), which finds 12-layer tracks by
adding extra hits to the identified tracks. In the designed configuration, 16
PUs and 4 SSBs are installed in a VME crate. The high power-consumption of the
AMB, AUX and SSB (respectively of about 250 W, 70 W and 160 W per board)
required the development of a custom cooling system. Even though the expected
power consumption for each VME crate of the FTK system is high compared to a
common VME setup, the 8 FTK core crates will use $\approx$ 60 kW, which is
just a fraction of the power and the space needed for a CPU farm performing
the same task. We report on the integration of 32 PUs and 8 SSBs inside the
FTK system, on the infrastructures needed to run and cool them, and on the
tests performed to verify the system processing rate and the temperature
stability at a safe value.

###### Index Terms:

Associative Memories, electronics cooling, FPGA, particle tracking,
temperature control, timing.

##  I Introduction

The VME boards developed for the Fast TracKer Processor (FTK) [1], an ATLAS
[2] trigger upgrade, perform the most power consuming task of the system. The
FTK is able to reconstruct, with high resolution, all of the tracks with
transverse momentum above 1 GeV within short latencies (few tens of
microseconds); it is compact (4 VME racks) and power usage is low ($\approx$
60 kW).

The FTK is organized in a pipelined architecture. A key role is played by high
performance FPGAs, while most of the computing power is provided by full-
custom ASICs named Associative Memories (AM) [3].

The 9U VME cards inside FTK are the “Associative Memory Board Serial Link
Processor” (AMB), the “Auxiliary card” (AUX) and the Second Stage Board (SSB).
The AMB, full of AM chips, is managed by the large Rear Transition Module
named the AUX card, full of powerful FPGAs. They sit in the same VME slot and
constitute (see Figure 1) a Processing Unit (PU). The PU is the FTK core that
solves the huge combinatorial task with pattern recognition. It is also the
most power and time consuming part of FTK.

Figure 1:  A PU is composed of one AMB (top) and one AUX card (bottom). In the
AMB picture, it is possible to distinguish the 4 LAMBs and the 64 AM chips.
The LAMBs in the picture show their internal face, in order to make it
possible to see the AM chips.

The AMB executes the low resolution pattern matching (PM) [4], working on 8
detector layers. It is based on the use of a large bank of pre-computed
patterns of trajectory points. The whole AM system stores 1 billion AM
patterns. It recognizes track candidates at low resolution to perform the
demanding task of tracking at the detector readout rate. The AUX validates or
rejects the track candidates found by the AMB by performing high resolution
track fitting (TF) [1]. The two functions PM and TF are executed in pipeline
and interfaced by the Data Organizer, which provides reduced resolution hits
to the PM and well-organized full-resolution hits to the TF. The PU output
(8-layers tracks) is sent to the SSB, which adds 4 extra detector layers to
produce 12-layer tracks.

The AMB is assembled with four mezzanines, the Little Associative Memory
Boards (LAMBs), for a total of 64 AM chips per board. The infrastructure
design for this compact and powerful system is described in Ref. [5].

Over 200 boards were produced, including 128 AUXs, 64 AMBs and 32 SSBs. Two
PUs and one SSB were included in 2018 ATLAS data taking. Two full VME crates
(32 PUs and 16 SSBs) were used for cooling tests.

##  II  Timing tests of the Integrated VME boards – Monitoring Tools

The monitoring of FTK-board dataflow is based on circular memories in the
firmware called Spy Buffers[4]. Circular memories are continuously written
with the data processed by the board unless a Freeze signal is asserted. When
the memory is frozen, it can be readout through VME bus for error diagnosis or
standard monitoring functions. The Freeze signal has been successfully used
during the tests to detect rare errors. It is activated on error conditions
and propagated to Freeze all of the involved spy buffers.

Other quantities are monitored during data processing: (a) to understand
pipeline bottlenecks the fraction of time each input FIFO is Empty or Half-
full is measured; (b) the event processing rate; (c) the temperatures, I/O
currents and power consumption for each power voltage; (d) specific tools
built for the AMB. For each event, the time needed to load data into the AM
chips and to send matched patterns to the output is measured for each I/O
stream. These measurements provide data for the pipeline studies, which is
crucial for ensuring the ability of the system to cope with the required
latency.

In the AMB, clusters (Hits) are received in parallel on 8 S-LINKs [6] (HIT
Time) and each Hit is distributed to all patterns with maximum fan-out: each
group of 8 Hits reaches all patterns in a single clock cycle. The track
candidates (Roads) found by the AM chips are readout in parallel on 16 S-LINKs
(Road Time). While the AM chips receive an event, the previous event is
readout from them in parallel. The End Event word (EE) declares the end of an
event download or an event readout to/from the AM chips.

The processing time is measured for all the 8 HIT links and the 16 ROAD links
using the same firmware module, the Time Monitoring Module (TMM). The
monitoring dedicated module measures the number of clock cycles between a
“Start” and a “Stop” signal.

Figure 2 shows the signals used to generate the “Start” and “Stop” signals of
the counters for both the HIT and ROAD link types. Both of the counters start
at the activation of the Send_Road signal sent by CONTROL to both the Hit and
ROAD links, to start the downloading of a new event and the readout of the
previous one. In the case of HIT links the time counter stops when the End
Event word is detected in all the links. The ROAD counter is stopped when the
End Event word has reached the OUT FIFO for each ROAD link.

Figure 2:  Sketch showing the portion of the AMB HIT and ROAD link logic where
the times are measured.

The link timings have been measured with simulated random events. Figures 3
and 4 show the results of the time measurements for data transit in the AMB on
each input (Figure 3) and output (Figure 4) event. The events and the set of
patterns stored in the AM chips were picked such that roads were constrained
to fire in the position of the AM pipeline where the latency is maximum (worst
case).

The input links have a time significantly smaller than the output links. The
lowest measured time for the output links is around 500 clock cycles,
corresponding to events with no matched roads. In fact, the output chip was
programmed to count 500 clock cycles at the AM chip output after the last
received road before declaring “Ended” the event to avoid the loss of roads
delayed inside the Associative Memory pipeline. The delay to get data through
the daisy chain and ROAD output logic explains the extra clock cycles that
separate empty and not empty events.

Figure 3:  Input link time distribution measured with simulated random events.

These timing studies allowed us to significantly decrease the conservative 500
clock cycles count originally set for the End of Event identification,
bringing the new value to 50 clock cycles. This change significantly reduces
the output link times.

Figure 4: ROAD output link times as a function of number of matched roads.

In conclusion, these measurements show that the AMB latency meets the timing
requirements for a 100 kHz event processing rate.

##  III VME boards power consumption

Since the power consumption of the board components changes based on their
configuration, a direct measurement is made rather than relying on predictions
from the manufacturers. The resource utilization (in typical FPGA designs,
some of the resources are not used after the configuration and thus they do
not consume any power) and the switching activity (the number of signal
transitions in a clock period) are the main contributors to the power
variation.

The power consumption of the AM chips also requires a careful measurement. In
this element, the power consumption is not related to its configuration, but
to the rate and composition of the data being processed.

Being FPGA-based, the power consumption of the AUX and SSB boards during
operation can be considered quite stable. Therefore, the variations upon the
different running conditions are small. The measurements have been performed
by programming the two boards with the latest stable firmware (FW) versions
(end of 2018), and running them in standalone (not connecting them to the up-
stream/down-stream boards) while processing simulated data. The AUX boards,
running in loop mode on data directly loaded on the FPGAs FIFOs, have been
measured to consume about 70 W. The SSB boards, fed with data coming from an
emulator connected to the board, have been measured to consume about 160 W.
Since no relevant changes in the FPGA resources utilization or in the
switching activities are expected, these values can be considered to be close
to the operational ones.

The estimation of the power consumption of the AMB relies on its two different
processing components: FPGAs and AM chips. While, as for the AUX and SSB case,
the AMB FPGAs are characterized by an almost fixed power consumption (for a
given FW version), the AM chips show drastic variations. As already mentioned,
these variations are related to the characteristics of the data undergoing
processing, and in particular to the input data rate and to the Bit Flip
number (BF), i.e. the number of bits that flip in the AM memory lines during
the pattern matching procedure. The total AMB power consumption can be,
therefore, computed as:

$AMB_{\text{power}}=AMB_{\text{core}}+4\cdot(LAMB_{\text{core}}).$ (1)

where $AMB_{core}$ represents the power consumption of the AMB mother board
alone (FPGAs component), while $LAMB_{core}$ represents the power consumption
of the LAMB boards, which is data dependent (AM chip component). The
$AMB_{core}$ value has been measured to be about 100 W. The $LAMB_{core}$ is
in turn the sum of two different contributions.

The first contribution comes from the dummy hit value, a 32-bit word that is
sent to the AM chip, alternated to the IDLE word, during the IDLE state to
avoid a strong current reduction when no or too few real data are available.
Because of the high data fan-out in the memory bank, the current on the AM
chip net is not constant, but varies from a quiescent current of 20 A to a
peak current of 220 A in a few hundreds of nanoseconds. A very powerful DC-DC
converter is used to power each LAMB, but even with this device it is not
possible to avoid the effect of the fast large peak of current, resulting in a
drop of the voltage level. In order to mitigate this problem, a dummy word is
sent to the AM chips while in IDLE, i.e. while it is not processing data,
helping to increase the quiescent current and, thus, reducing the voltage
drop. The dummy word doesn’t fire any pattern on the chip, but can be chosen
so that the number of bits that flip in the AM lines at each clock cycle can
be tuned as desired, managing the IDLE power consumption of the chip. The
choice of the value of the dummy hit is finally a compromise between the
increase of the quiescent current of the chip net, requiring a big bit flip
value, and the necessity of reducing the total power consumption of the board.

The dummy hit value selected as optimal for operations corresponds to a BF
value of $3.5$. In Figure 5 the result of the measurements performed to
characterize the IDLE power consumption using this dummy hit is presented,
showing a value of about $25$ W.

Figure 5:  LAMB power consumption for a value of dummy hit of 0x7a007500
(corresponding to a bit flip of 3.5). During this measurements no data were
sent to the AM chips, the resulting power consumption is only due to the dummy
hit.

The second component contributing to the LAMB power consumption is the mean
number of bit flips inside the data and the rate at which these data are sent
to the AM chips for comparison. From the expected FTK running conditions, the
maximum value for the data word undergoing matching in the chips is
represented by a 13-bits word. Considering continuous data with random data
words distributed flat between 0–8191 (using 13 bits), the power consumption
of the LAMB has been measured to be about 48 W. This value has been measured
feeding the AMB with continuous simulated data, ensuring no dummy hit
contribution to the power consumption value.

In order to have a conservative estimation of the rate, the worst case
scenario for the FTK running condition has been considered. From simulations,
considering a pile-up value of $\mu=57$, the maximum number of clusters among
the different FTK regions and detector layers is expected to be 340
clusters/layer. This value was used for the computation of the power
consumption, giving a $22\%$ margin over the mean value on the different
detector layers. It is important to notice that the cluster number does not
depend on the set of patterns stored in the AM chips, but only on the detector
geometry and pile-up. Using a linear approximation for the scaling of the
number of clusters with the pile-up, a number of 360 clusters/layer is
considered for the $\mu$ = 60 operation case.

Assuming a mean number of 360 clusters to be processed every 10 $\mu$s at
$\mu$ = 60, and given a 100 MHz clock cycle for the AM chips, 36% of the
cycles are spent processing data with a power consumption of 48 W. The
remaining cycles are spent in IDLE mode with the board consuming the 25 W
given by the dummy hit. The resulting total AMB power consumption at a pile-up
$\mu$ = 60 is

$AMB_{\text{power}}=100\>W+4\cdot(48\>W\cdot 0.36+25\>W\cdot 0.64)\approx
233\>W$ (2)

with a mean LAMB power consumption of about 33 W. The total VME rack power can
be computed as the sum of the different board’s powers, plus the custom fan
tray system measured to consume 3.4 kW per VME rack. In Table I, a summary of
the various VME components power consumption is shown. Considering a 90 %
efficiency for the power supply ($PS_{eff}$), the total VME rack power is:

$\begin{split}&Rack_{\text{power}}=(((AUX_{\text{power}}+AMB_{\text{power}})\cdot
16+\\\ &+SSB_{\text{power}}\cdot 4)\cdot 2+Fan_{\text{power}}\cdot
2)/PS_{\text{eff}}\approx 16\>kW\end{split}$ (3)

TABLE I: Table summarizing the power consumption of the different FTK VME components of each FTK rack. FTK VME component | Power (W) | Component number
---|---|---
AUX | 70 | 32
SSB | 160 | 8
AMB | 212-244 | 32
Fan tray | 850 | 4
Full rack | $\approx 16000$ |

The standard VME cooling, coupled with the standard rack water cooling system,
is not powerful enough to dissipate a total power of $\approx$16 kW. A custom
cooling system based on powerful fan trays has therefore been adopted.

##  IV Temperature limits and cooling infrastructure

Each board component has a given temperature range in which its safe operation
is guaranteed. The maximum temperature threshold is generally provided by the
manufacturer of the given component. Keeping the temperatures low during
operation also increases the lifetime of the boards, reducing the risk of
failures. Given the high number of FPGAs (about 2000 elements) and of ASICs
(about 8000 AM chips) that compose the FTK system, reducing the component
failure risk is of primary importance for the project itself.

For AUX and SSB the temperature limit is driven by the processing FPGAs. The
AUX board is equipped with 6 commercial Altera Arria-V FPGAs [8]. This FPGA is
rated to an operational temperature limit of 85 ∘C. No damages to the
component are expected for temperatures up to 125 ∘C. The SSB board power
consumption is driven by 4 Xilinx Kintex-7 FPGAs [9]. Version 4 (V4) boards
use commercial FPGAs rated to 85 ∘C, and a second production (V5) use
industrial FPGAs rated to 100 ∘C. The AMB is equipped with 4 FPGAs. The HIT
and ROAD chips are commercial Xilinx Artix-7 FPGAs [9], rated to an
operational temperature threshold of 85 ∘C. The AMB data control logic is
instead based on two Xilinx Spartan-6 FPGAs [10], that present the same
temperature thresholds. For both FPGA versions, no damages are expected for
temperatures up to 125 ∘C. Beside the FPGA limits, the most temperature
sensitive elements are the AM chips. Being a custom element, an exhaustive
data sheet is not available. Estimations have rated the AM chips to be damage-
safe up to 100 ∘C, but a conservative operational temperature threshold has
been set to 80 ∘C.

A protection system has been put in place to prevent possible damage from
overheating. This system relies on two different components.

The first component is a FW protection, able to immediately stop the board
dataflow in case the measured temperature is found to surpass a given
threshold. While the FPGA temperatures are directly measured by the components
themselves, the AM chips measurement relies on temperature sensors placed
around the AM chips, on the LAMBs. This protection stops the data sent to the
AM chips in a whole LAMB, letting the temperature decrease.

In addition to the FW component, the second one is a software (SW) protection,
managed by the ATLAS DCS (Detector Control System [11]) and able to shutdown a
VME crate in case of problems. In general, the DCS is a highly distributed
system that is used to supervise and monitor the ATLAS experiment
infrastructure. The FTK DCS is used to control and monitor the FTK
infrastructure, retrieving data such as the board temperature, the air
temperature in the crate and in the fan trays, the fan speeds and the power
supply parameters. In addition, the FTK DCS manages the cooling system in
response to the retrieved data, as well as managing the PS emergency
interlocks. Exploiting this, the DCS has been programmed to read the rack air
temperature, and to trigger the PS interlock in case the read value surpasses
a given threshold. The interlock shuts down the power to the crate, keeping
only the power to the cooling system (the fan trays). The rack air temperature
threshold at which the DCS triggers the shutdown was preliminarily set to 32
∘C but, as a result of the cooling tests, described later, was finally
increased to 38 ∘C.

In order to dissipate a power of more than $\approx 16$ kW, six 1U heat
exchangers are mounted in each VME rack. The heat exchangers are cooled by
means of a cold water flow injected at 14 ∘C, with a pressure $\Delta P=4.5$
bar. These heat exchangers, in the given configuration, are proven to be able
to dissipate 3.8 kW of power each [7]. The high number of heat exchangers
needed increases the air resistance in the rack. Together with the high board
density (increasing the air flow resistance as well), this poses the
requirement of powerful fans, able to help the cooling system by increasing
the air flow and its uniformity between the different crate slots.

Four custom-made fan trays, composed of nine powerful fans (able to run with a
speed above 10.5 krpm) have been developed and produced. The choice of custom
fan trays is driven by the fact that the commercially available ones do not
provide enough air flow through the rack components, as demonstrated in
studies performed during the development phase of the FTK VME cooling
infrastructure [5].

In the final FTK VME cooling system composition, each VME rack is equipped
with the six heat exchangers, the standard rack turbine, and with four of the
custom fan trays, placed just under/above the crates. Figure 6 shows a sketch
of the final VME rack configuration, together with a real picture of a fully
populated rack.

Figure 6: Sketch representing the VME rack configuration, together with a
picture of a fully populated rack.

The nine fans of each fan tray are organized into three rows of three fans
each, two rows in the front of the rack, where the AMB and SSB boards are
located, and one row on the back, where the AUX cards are placed. Electronic
control and monitoring are implemented with an Arduino microcontroller, Mega
2560 type, equipped with a local display for every fan tray. Local/remote
ON/OFF is available, and four speeds (40%, 60%, 80%, 100%) are settable
independently within the three rows of fans. Six temperature sensors are
positioned inside the fan tray to monitor the environmental temperature. The
fan speed selection is controlled, through the Arduino, by the DCS system. The
speed of the fans is automatically managed and increased/decreased by the DCS
with the increase/decrease of the temperatures measured inside the fan trays.

For testing purpose only, a chiller, able to further cool down the water
entering the rack existing cooling system (i.e. to the heat exchangers), was
also provided for the FTK racks. A set of tests with this cooler water were
performed, but the tests shown later demonstrate its use is not necessary.

##  V FTK VME Cooling tests

In order to prove the performance of the cooling infrastructure, a series of
cooling tests were performed, reproducing the board working conditions
expected during the FTK operation.

The cooling tests have been performed using one of the VME racks fully
equipped, with an FTK power supply, two VME crates fully loaded with boards,
and the final version of the cooling system. Figure 7 shows a sketch of the
boards positions inside the testing crates.

Figure 7: Sketch of the VME crates used during the cooling tests. The slots of
each crate in which the 16 PUs and the 4 SSBs are placed are shown. Only one
V4 SSB was used during the tests, placed in slot 16 of the bottom crate.

For the tests, the AUX cards ran a loop over simulated data directly loaded in
the input FIFOs. The power consumption of this board was about 70 W. The two
versions of SSB boards were used. However, only one V4 SSB was available for
the tests. All the SSBs were running on data provided by an emulator, directly
connected to the boards by the respective RTM cards. The power consumption of
these boards was about 160 W. The AMB boards were run in loop mode on
different sets of simulated data. The different data sets were produced with
different predefined bit flip values (6, 6.5 and 7), in order to select a
different power consumption of the AM chips for each of the measurements. For
sake of brevity, only the tests performed with simulated data representing a
BF value of 6, corresponding to the expected FTK operation conditions, will be
presented. In Figure 8, the distribution of the LAMB power consumption for the
testing data is presented. The measured 33 W per LAMB corresponds to the
expectations presented in the previous section.

Figure 8: Distribution of the LAMB power consumption for the BF = 6 simulated
data.

At the time of the tests, the board’s temperature information was only
accessible through custom command line tools, not integrated in the FTK online
software. A python wrapper of these tools has been developed and used for the
measurements. This wrapper was able to read directly from the boards’ FPGAs
the temperature registers and to perform the conversions required. Each
measurement was performed in intervals of about 300 s. In order to have a
direct measurement of the AMB power during the tests, the AMB DC/DC converters
values of current and voltage were also measured. This was not required for
AUX and SSB, which show stable power consumption.

The temperature of the fan trays and of the rack air was also measured. The
data in this case were directly retrieved from the DCS. The DCS was also used
to provide the values of the power provided during the tests by the rack power
supply. This information was useful in order to perform a cross check between
the power expected from the AUX and SSB boards and the measured power consumed
by the AMBs.

Moreover, during the tests both the DCS safety system and the automatic fan
speed control were disabled. The former was due to a temperature threshold
initially set too low for the most demanding tests. The latter was triggered
to study the temperature profile of the boards on different values of the fan
speeds, that were set manually to a different value on each test.

Figure 9: Temperature profile of the hottest LAMB of each AMB for the top VME
crate (a) and bottom VME crate (b). The AMB operational temperature limit is
80 ∘C. In this configuration all the temperatures are well under control.

Figure 9 shows the temperature profile of the hottest LAMB of each crate slot,
for the upper (a) and lower (b) crates. From both plots it is possible to note
an initial rapid increase of the maximum temperatures, due to the heating up
of the boards. This increase stops just after the second measurement, where
the plateau is reached. In this configuration, the temperatures are well under
the operational temperature limit. From the comparison of the two crate
results, the upper crate temperatures are slightly lower than the lower crate
ones. This is expected due to the position of the heat exchangers inside the
rack. As can be seen in Figure 6, only two heat exchangers will cool down the
air coming from the upper VME crate, while four of them are placed between the
lower and the upper crates. A solution to this problem would be to move one of
the heat exchangers that are surrounding the PS to the very bottom of the
rack, just after the air deflector. Since the difference in the temperatures
between the two crates is small, this is not considered an issue.

Figure 10 shows the same measurements performed on the AUX cards (a) and on
the SSB boards (b). For the sake of brevity, only the lower crate measurements
(the hottest crate) are presented. Due to the low power consumption of this
kind of boards, the temperatures are very stable. No increase is seen in the
AUX temperatures because the first measurement is only made after the AMBs, so
only the plateau is seen. The AUX cards are in the back of the crates, and
therefore do not directly see the heat from the AMB and SSB.

Figure 10:  Temperature profile of the hottest FPGA of each AUX (a) and SSB
(b) for the lower VME crate. The slot 16 of the crate is equipped with the
only V4 SSB used during the tests. All the temperatures are well under
control.

The SSB the measurements were performed after the AMB ones, thus, only the
plateau can be observed. The single V4 SSB used in the test is placed in slot
16 of the lower crate. The SSB placed in slot 21 shows temperatures of about 6
∘C higher than the other boards. This is due to a non perfect distribution of
the air flow inside the crate.

To better understand this problem, Figure 11 shows the same test measurements,
but including the temperatures of all four SSB FPGAs rather than only the
hottest one. In all the tests performed, the hottest FPGA of each crate has
always been the number 2 of slot 21. This FPGA is placed on the top back
corner of the SSB, the one most difficult to be reached by the air flow
produced by the fans. The FPGAs numbered 2 and 3 are usually hotter because
they are directly above the two lower FPGAs, numbered 0 and 1. Between the
lower FPGAs, the one placed in the back of the board is usually hotter than
the front one. These results inform the final position of the boards in the
crate as not much can be done to improve the airflow. A V4 SSB, for example,
will not be placed in slot 21, where the 80 ∘C measured are very close to the
operational temperature limit for that board. In summary, all the measured
temperatures are well under the operational temperature limit, for all the
board types.

Figure 11:  Temperature profile of the four FPGAs of each SSB for the bottom
VME crate. In the plot, each dashed line correspond to a different FPGA. The
FPGA number of which each line correspond is the same as its order of
appearance in the legend (e.g. continuous line: FPGA 0).

Since all the tests were performed in a single rack, a second set of tests
have been performed to study for possible rack to rack variations. Due to the
lack of available boards, the test was performed with only eight PUs and one
SSB per crate. In order to have coherent results, the same rack configuration
was used performing the measurements on two different racks. Figure 12 shows
the distribution of the LAMB temperatures for the two different racks tested.
The measured mean LAMB temperature of the new rack is 2 ∘C higher than the one
of the standard rack. In order to be conservative, a variation of 5 ∘C has
been considered as rack to rack variation for the final considerations on the
cooling test results.

Figure 12: Distribution of the LAMB temperatures running the AMB with BF = 6
simulated data for two different racks (a) and (b). The VME crates on each
rack were equipped with 8PUs and 1 SSB. A variation of 2 ∘C has been observed
between the two racks.

As a concurrent step to the cooling tests, optimization studies for both the
best fan speeds configuration and the rack air temperature tresholds have been
performed.

Varying the fan speed can cause differences in the air flux inside the racks,
and it can increase/decrease turbulence. Moreover, reducing the speed of the
fans can increase their lifetime. Tests, changing each time the settings of
the fan speeds, have been performed in order to study the best configuration.
The tests were performed in the rack used for the cooling tests, using 16 PUs
and 4 SSBs in each crate and using the speed configurations (fans at the top-
bottom of the crate) 100%–100%, 80%–100%, 60%–100%, 100%–80%, and 100%–60%.
The tests were also repeated for different AMB power consumption levels.

In all the tests performed, the lowest temperatures were measured in the fan
speed configuration 100%–60%. Running the bottom fan tray at a reduced speed
with respect to the top one helps to avoid the creation of turbulences and to
increase the uniformity of the air flux in the crate volume. Moreover,
reducing the fan speed would significantly increase its lifetime. For this
reason, the final fan speed of the FTK lower fans has been fixed to 60%,
leaving the speed of the top fans to be adjusted automatically by the DCS. In
this case its speed will vary from the lower 60% level to the maximum 100%
level as function of the temperatures read.

Finally, for the rack air temperature threshold optimization, tests running
the boards above the expected power consumption levels (in order to get closer
to the board temperature thresholds) have been performed. For these tests, the
fully populated rack used in the cooling test has been used, running the AMB
with BF = 7 simulated data, corresponding to a power consumption of 38 W per
LAMB. The maximum value of the air temperature obtained in this tests was 36
∘C. The maximum corresponding temperature for the LAMBs was 70 ∘C. Since the
test running condition is expected to be higher than the maximum condition
expected for the FTK operation, the selected threshold for the SW rack safety
system is 38 ∘C. This would leave some margin over the maximum air temperature
measured, still keeping the boards in a safe working condition.

##  VI Conclusions

Two FTK VME crates full of 16 PUs and 4 SSBs each have been successfully
installed, and the system performance has been tested using simulated data.
Even though the complete FTK processor’s power consumption ($\approx$ 60 kW)
is a fraction of its CPU equivalent, its power density is much higher. This
results in an unusually large power consumption per VME crate and the need for
a complex custom solution in order to ensure sufficient cooling. Extensive
studies have been performed to investigate the system power consumption in
real running conditions, and the ability of the developed cooling
infrastructure to cope with the big power densities to be dissipated. Thanks
to these studies and optimizations, the cooling infrastructure is proven to
sufficiently cool the FTK processors under the worst case scenario. Moreover,
the processing latencies were reduced based on the timing studies performed.
The measurements performed demonstrate the timing requirements for a 100 kHz
event processing rate are met.

## References

##

  * [1] ATLAS Collaboration, “The Fast Tracker (FTK) Technical Design Report”, CERN-LHCC-2013-007 ; ATLAS-TDR-021; available online: https://cds.cern.ch/record/1552953.
  * [2] ATLAS Collaboration, “The ATLAS Experiment at the CERN Large Hadron Collider”, Journal of Instrumentation 3 S08003, 2008.
  * [3] M. Dell’Orso and L. Ristori, “VLSI Structures Track Finding”, Nucl. Instr. and Meth. A, vol. 278, pp. 436-440, 1989.
  * [4] S. Citraro et al., “Highly Parallelized Pattern Matching Hardware for Fast Tracking at Hadron Colliders”, IEEE Trans. on Nuclear Science, Volume: 63, Issue: 2, pp. 1147 - 1154 2015, 2016.
  * [5] C. -L. Sotiropoulou et al., “The Associative Memory System Infrastructures for the ATLAS Fast Tracker”, IEEE Trans. on Nuclear Science, Volume: 64, Issue: 6, pp. 1248 – 1254, 2017.
  * [6] H.C. van der Bij et al., “S-LINK, a data link interface specification for the LHC era”,1996 IEEE Nuclear Science Symposium. Conference Record, CERN-EP-2019-242, 1996.
  * [7] G. Thomas., “Rack Cooling Project - Final report.”, In: (Aug. 2002), available online: http://cds.cern.ch/record/38031.
  * [8] Altera, “Arria V FPGA and SoC Features”, available online: https://www.intel.com/content/dam/www/programmable/us/en/pdfs/literature/pt/arria-v-product-table.pdf.
  * [9] Xilinx Incorporated, “7 Series FPGAs Data Sheet: Overview”, available online: https://www.xilinx.com/support/documentation/data_sheets/ds180_7Series_Overview.pdf.
  * [10] Xilinx Incorporated, “Spartan-6 Family Overview”, available online: https://www.xilinx.com/support/documentation/data_sheets/ds160.pdf.
  * [11] S. Schlenker et al., “The ATLAS Detector Control System”, available online: https://accelconf.web.cern.ch/icalepcs2011/papers/mobaust02.pdf


# Parallel Verification of Natural Deduction Proof Graphs

James T. Oswald Brandon Rozek  Rensselaer AI & Reasoning (RAIR) Lab,
Rensselaer Polytechnic Institute (RPI)
Troy, New York, USA {oswalj<EMAIL_ADDRESS>
###### Abstract

Graph-based interactive theorem provers offer a visual representation of
proofs, explicitly representing the dependencies and inferences between each
of the proof steps in a graph or hypergraph format. The number and complexity
of these dependency links can determine how long it takes to verify the
validity of the entire proof. Towards this end, we present a set of parallel
algorithms for the formal verification of graph-based natural deduction
($\mathcal{N\mkern-4.0muD}$ ) style proofs. We introduce a definition of
layering that captures dependencies between the proof steps (nodes). Nodes in
each layer can then be verified in parallel as long as prior layers have been
verified. To evaluate the performance of our algorithms on proof graphs, we
propose a framework for finding the performance bounds and patterns using
directed acyclic network topologies (DANTs). This framework allows us to
create concrete instances of DANTs for empirical evaluation of our algorithms.
With this, we compare our set of parallel algorithms against a serial
implementation with two experiments: one scaling the problem size and the
other scaling the number of threads. Our findings show that parallelization
results in improved verification performance for certain DANT instances. We
also show that our algorithms scale for certain DANT instances with respect to
the number of threads.

##  1 Introduction

A major role of an interactive theorem prover is to take an existing proof and
verify that it is valid with respect to the logical calculi used. This
involves iterating over each step of a proof and verifying both that it
syntactically matches the transformation of the formula under the rule, and
that it is valid with respect to the semantics of the underlying proof system.
Interactive theorem provers such as Coq [20], Lean [15], and HyperSlate [5]
verify not only that the proof written by the user is correct, but also every
underlying proof that the given proof depends on. This generally amounts to
verifying large portions of the standard library and other popular libraries
such as mathlib [7]. Our work makes a step toward speeding up the proof
verification process. We focus on the verification of natural deduction proof
graphs, such as those represented in HyperSlate, though the ideas from this
approach could be adapted to other interactive theorem provers as well.

In order to speed up verification, we look toward parallel computing. One
naive implementation would be to verify all the proof steps in parallel. This
assumes, however, that the step has all the semantic information needed to
show validity. This is often not the case for many logic calculi. Assumptions
are introduced and discharged in the case of natural deduction. Variables may
be assigned to constants. These issues present a constraint that in order to
parallelize verification, we need to ensure that some steps are verified
before others. We achieve this by introducing a layering approach. Given a
definition of layering that induces a topological partial order, every step
within a layer $n$ only depends on steps within the layers prior. Given these
layers, we can then verify all the steps that are from the same layer in
parallel without worrying about invalidating the underlying semantics. To
illustrate this approach, we present the parallel verification of natural
deduction proof graphs.

The underlying dependency nature of each of the steps induces a directed
acyclic hypergraphical representation where nodes hold
$\mathcal{N\mkern-4.0muD}$ statements and hyperedges between nodes represent
inference rules. This graphical representation not only gives us an easy way
to visualize such proofs, but also provides insight on empirically validating
our parallel algorithms. Inspired by computer network topologies, we introduce
directed acyclic network topologies (DANTs) as a way to identify classes of
graphical proofs. These topologies provide a method of comparing the
performance of different verification strategies on various proof structures.

The contributions of this work are as follows: (1) A layering approach that
decouples the dependencies of proof steps within $\mathcal{N\mkern-4.0muD}$
proofs. (2) Parallel verification algorithms that outperform serial
verification on non-straight topologies and scales with the number of
hardware-based threads. (3) Introduction of several classes of graphical
proofs, with an eye on empirical evaluation. The relevant background which
includes $\mathcal{N\mkern-4.0muD}$ and hypergraphical representations is
discussed in §2. Within §3, we discuss the proof verification algorithm and
several optimizations. Then in §4, we discuss directed acyclic network
topologies to empirically evaluate common proof structures. In that section,
we also discuss our performance and scaling results. We then conclude by
talking about related work in §5.

##  2 Background

###  2.1 Natural Deduction

Natural deduction ($\mathcal{N\mkern-4.0muD}$ ) is a logic calculus
independently proposed in [11, 13] in an effort to emulate human-level
reasoning through assumptions and chains of inference. There are many
different styles of proof that fall under natural deduction, the three most
common come from Gentzen [11], Jaśkowski [13], and Fitch [10]. However, we are
mainly interested in a style that interoperates with a hypergraphical
representation of natural deduction proofs.

$\displaystyle\\{\phi\\}\vdash\phi\quad\quad\Gamma\cup\Sigma\vdash\phi\land\psi\Gamma\vdash\psi\quad\Sigma\vdash\phi\quad\quad\Gamma\vdash\phi\Gamma\vdash\phi\land\psi\quad\quad\Gamma\vdash\psi\Gamma\vdash\phi\land\psi$
$\displaystyle\quad\quad\Gamma\vdash\psi\lor\phi\Gamma\vdash\phi\quad\quad\Gamma\vdash\phi\lor\psi\Gamma\vdash\phi\quad\quad\Delta\cup\Gamma\cup\Sigma\vdash\chi\Delta\vdash\psi\lor\phi\quad\Gamma\cup\\{\psi\\}\vdash\chi\quad\Sigma\cup\\{\phi\\}\vdash\chi$
$\displaystyle\quad\quad\Gamma\vdash\phi\rightarrow\psi\Gamma\cup\\{\phi\\}\vdash\psi\quad\quad\Gamma\cup\Sigma\vdash\psi\Gamma\vdash\phi\quad\Sigma\vdash\phi\rightarrow\psi$
$\displaystyle\quad\quad\Gamma\cup\Sigma\vdash\lnot\phi\Gamma\cup\\{\phi\\}\vdash\psi\quad\Sigma\vdash\lnot\psi\quad\quad\Gamma\cup\Sigma\vdash\phi\Gamma\cup\\{\lnot\phi\\}\vdash\psi\quad\Sigma\vdash\lnot\psi$
$\displaystyle\quad\quad\Gamma\cup\Sigma\vdash\phi\leftrightarrow\psi\Gamma\cup\\{\phi\\}\vdash\psi\quad\Sigma\cup\\{\psi\\}\vdash\phi\quad\quad\Gamma\cup\Sigma\vdash\psi\Gamma\vdash\phi\quad\Sigma\vdash\phi\leftrightarrow\psi\quad\quad\Gamma\cup\Sigma\vdash\phi\Gamma\vdash\psi\quad\Sigma\vdash\phi\leftrightarrow\psi$
Figure 1: Our inference schemata for natural deduction. Within each schema,
$\Gamma,\Sigma,\Delta$ are sets of formulae, and $\phi,\psi,\chi$ are meta-
logical variables which range over formulae. Note that our formulation of
$\lnot I,\lnot E,\leftrightarrow I,\leftrightarrow E$ differs from those
typically seen in other works such as [18] but are equivalent.

In this paper, we focus on propositional natural deduction. Let $p$ denote an
atomic proposition. The language of propositional logic may be defined
inductively using Backus Naur Form (BNF) as the following:

$\phi::=p|\neg\phi|(\phi\wedge\phi)|(\phi\vee\phi)|(\phi\rightarrow\phi)|(\phi\leftrightarrow\phi)$

Our inference rules for $\mathcal{N\mkern-4.0muD}$ are summarized in Figure 1
111While on the surface this formalization may appear similar to sequent
natural deduction[17], we use “$\vdash$” in this formalism to mean syntactic
entailment, with $\Gamma\vdash\phi$ being read as ”Assuming $\Gamma$, then
$\phi$” or ”$\phi$ can be derived from $\Gamma$”.. This formalization is
modeled after Bringsjord [4] and fully captures the notion of discharging of
assumptions. It is also particularly well suited to hypergraphical
representation, which will be discussed in §2.2. These inference rules can be
broadly split into two categories: (1) introduction rules ($\land I,\lor
I_{l},\lor I_{r},\lnot I,\rightarrow I,\leftrightarrow I$), in which a logical
connective is introduced into the conclusion, and (2) elimination rules
($\land E_{l},\land E_{r},\lor E,\lnot E,\rightarrow E,\leftrightarrow
E_{l},\leftrightarrow E_{r}$), in which a connective in a rule’s premise is
removed in its conclusion. The outlier here is the Assumption rule (A) which
allows us to assert $\\{\phi\\}\vdash\phi$, or in English, ”assuming $\phi$,
$\phi$ follows”.

For a natural deduction proof, a step is considered valid if the formula is
well-formed and it is justified by a rule of inference. Valid formulae with no
assumptions are called tautologies. A proof is considered valid iff all of its
steps are valid. An example of a valid proof can be seen in Figure 2.

$\\{A\lor B,\lnot A\\}\vdash B\\{A\lor B\\}\vdash A\lor B\quad\\{\lnot
A,A\\}\vdash B\\{\lnot B,\lnot A\\}\vdash\lnot A\\{\lnot B,\lnot
A\\}\vdash\lnot A\land\lnot B\\{\lnot A\\}\vdash\lnot A\quad\\{\lnot
B\\}\vdash\lnot B\quad\\{A\\}\vdash A\quad\\{B\\}\vdash B$ Figure 2: An
example of a valid proof of $B$ from $\\{A\vee B,\neg A\\}$. All steps are
valid since at each step (1) all formulae are well formed and (2) the provided
rule of inference can be legally applied at each stage given the current
assumptions and premises.

###  2.2 Hypergraphical Representation

Figure 3: Visualizations of 4 different types of graphs, note that in the
hypergraph, edges that share the same color are the same edge.

A natural deduction proof can be represented diagrammatically as a directed
acyclic hypergraph [21, 2]. A directed acyclic hypergraph is a generalization
of a directed acyclic graph (DAG) which is a mathematical structure $(V,E)$
where $V$ is a set of vertices and $E:(V\times V)$ is a set of pairs of
vertices. Acyclic in this context means that for any vertex $v$, it is not
possible to find a path following the directed edges that leads to $v$.
Directed acyclic hypergraphs extend this by allowing a set of vertices to be
connected to a set of vertices by a single edge, thus a directed acyclic
hypergraph is a structure $(V,E)$ where $V$ is a set of vertices and
$E:\mathcal{P}(V)\times\mathcal{P}(V)$, where $\mathcal{P}(V)$ is the power-
set of the set of vertices. Figure 3 shows visualizations of the three graph
formalisms described.

To represent natural deduction proofs as hypergraphs, vertices represent
premises and conclusions, and edges represent inference rules. A proof graph
will be defined as a hypergraph of the form $(V,E)$ where $V$ is a set of
statements in the form $\Gamma\vdash\phi$ and $E:\mathcal{P}(V)\times V$ is
the set of directed hypergraphical edges representing inference rules applied
between statements in the proof.222Note we use $\mathcal{P}(V)\times V$ rather
than $\mathcal{P}(V)\times\mathcal{P}(V)$ since for all inference rules
enumerated in Figure 1 there is only one conclusion, thus each hyper-edge
representing an inference rule will only ever have one outgoing connection.
This formalism underlies the representation of proofs in graphical interactive
theorem provers such as [5, 16]. Figure 4 provides examples of two natural
deduction proofs that have been converted to hypergraphical form.

Interactive theorem provers often do not force the user to keep track of proof
state. Therefore, it is important to note that we are interested in verifying
proof graphs where the assumptions on each node are yet to be known. We are
only given the $\phi$ on each node and must compute the $\Gamma$ based on how
the assumptions update within the inference rules. If we had both $\Gamma$ and
$\phi$, parallelization would be trivial, since we can then verify all the
nodes in parallel.

$\\{\lnot(p\lor q)\\}\vdash\lnot p\\{p\\}\vdash p\lor q\\{p\\}\vdash
p\quad\\{\lnot(p\lor q)\\}\vdash\lnot(p\lor q)$

Figure 4: (Top Left) A valid natural deduction proof that $\\{\lnot(p\lor
q)\\}\vdash\lnot p$ (Bottom Left) The same proof represented as a
hypergraphical proof graph structure in the Lazyslate interactive theorem
prover[16]. (Right) Proof graph of the proof from Figure 2 of $\\{A\vee B,\neg
A\\}\vdash B$ in the HyperSlate [5] interactive theorem prover.

Proof graphs implicitly provide additional useful features for representing
collections of natural deduction proofs, particularly those that are commonly
added onto natural deduction via additional formalisms. First, proof graphs
provide the ability to compactly represent proofs that contain reoccurring
subproofs. This is because each hyper-node may have multiple outgoing hyper-
edges, representing multiple inferences it is used in. While this feature is
implicitly captured by proof graphs, natural deduction proofs require an
additional formalism allowing named theorems that can be used in other proofs
to provide this functionally. Another feature is that a single proof graph can
have multiple conclusions or even contain multiple proofs where each proof is
a disjoint hyper-subgraph. Without proof graphs, the ability to represent this
feature would require a formalism in which a set of proofs can be be treated
as a single proof.

###  2.3 Multiprocessing

In this work we use a shared memory model for multiprocessing. This involves
multiple threads independently operating over the same shared memory space.
More specifically, we make heavy use of single program multiple data (SPMD)
style programs. With a fixed number of threads instantiated, we attempt to
distribute work evenly across all the threads. Our work makes use of two
important concepts from multi-processing: thread-safety and reductions (see
[14] for more extensive coverage). Thread-safety within a shared memory model
is the notion that parallel algorithms are safe from errors due to concurrent
writes and reads from the same piece of memory, known as a race condition. The
second concept is the notion of a parallel reduction. A parallel reduction is
an operator that takes a list of elements and computes a single element in
parallel. A small example of this would be parallel sum over the list
$(1,2,3,4)$: if we add 1 and 2 on one thread and 3 and 4 on another thread in
parallel, and then sum their results, we can sum the entire list in 2 steps
rather than the 3 steps it would take to sum the list in serial.

##  3 Approach

We mentioned in §2 that natural deduction makes use of assumptions and chains
of inference in its proofs. In the hypergraphical representation, to show that
a given node is valid, we need to show both that the _syntactic
transformation_ is valid and that the _assumption constraints_ are met with
respect to the justification used inside that proof. Let us consider the rule
disjunction elimination (more commonly known as proof by cases) from Figure 1
and its usage in the right proof of Figure 4. For example, we wish to show
that bottom node $B$ is valid. For the syntactic check, we need to ensure that
there are three parent nodes, one of them is a disjunct, and two of the other
parent nodes match the current node. Then for the assumption constraints, we
need to make sure that for one parent node $B$ it has $A$ in its assumption
set, and for the other parent node $B$ it has $B$ in its assumption set. Note
from our discussion of the hypergraphical representation in §2.2 that the
underlying nodes do not contain the assumption information themselves, but
they are computed by the application of each inference rule. This creates the
need of an additional data structure that we call assumptions during the
verification process. We obtain the justification of a given step by calling
just on the node. This will return the justification that is stored on the
incoming edge of the node.

For a baseline comparison with the parallel verification algorithms, we
designed a single-threaded implementation that shares the same algorithmic
structure as the parallel ones minus the usage of shared memory and threading.
The benchmark results are further discussed in §4. Our algorithm works by
maintaining a global map of nodes to their set of assumptions. To ensure that
a node does not get verified before its parent, we make use of a layering
approach which induces a topological partial ordering on the nodes. A
topological partial ordering, also referred to as topological generations, of
a proof graph $G=(V,E)$ is a partial ordering $\preccurlyeq$ on the nodes $V$
where for each hyperedge $(\\{v_{i0},\cdots,v_{in}\\},v_{o})$, all incoming
nodes $\\{v_{i0},\cdots,v_{in}\\}$ appear before the outgoing node $v_{o}$,
that is $\forall(V_{i},v_{o})\in E:\forall v_{ij}\in V_{i}:v_{ij}\preccurlyeq
v_{o}$. This layering approach for generating a topological partial ordering
is similar to the well known serial topological sort algorithm [8] which
generates a topological linear ordering of the nodes but lacks
parallelizability. Figure 5 provides a colored example of the nodes on each
layer. More formally, we define node $n$ to be on a layer $L(n)$ inductively
as follows:

$L(n)=\begin{cases}0&\text{if $n$ is an assumption}\\\ 1+\max_{m\in
P(n)}(L(m)),&\text{otherwise}\end{cases}$ (1)

where $P(n)$ maps a node to its parents.

###  3.1 Single-Threaded Implementation

Algorithm 1 Single-Threaded Algorithm

1:procedure verify(ProofGraph p)

2: Initialize assumptions to be empty.

3: Create set of nodes on each layer using Equation 1 and store in layerMap.

4: for layerNodes in layerMap do

5: for n in layerNodes do

6: justification = just(n)

7: ruleInfo = (m, assumptions(m)) $\forall$ m $\in$ parents(n)

8: if not is_valid(n, justification, ruleInfo) then

9: return false

10: Update assumptions(n) using the justification and ruleInfo.

11: return true

The full single-threaded procedure is described in Algorithm 1. For every
layer, the procedure performs the following actions: (1) Verify that the node
is valid with respect to the justification claimed using the node’s and its
parents’ syntactic information and the parents’ assumption information. (2) If
valid, update the assumptions data structure for the current node based on the
parents’ assumptions and justification.

In order to better highlight the progression of the algorithm, we will walk
through an example by looking at the verification of Figure 4 (Right).
Subscripts for the propositions help to distinguish between formulae by
referencing the ID denoted inside the purple box in the figure. In the
beginning of the algorithm, the first layer only contains assumptions:

$\texttt{currentLayer}=\\{(\neg A)_{1},(\neg B)_{2},A_{5},B_{7},(A\vee
B)_{8}\\}$

We then go through each node and verify them. Since they are justified as
assumptions, they are trivially valid. The nodes then have their assumptions
updated. The next layer only contains $(\neg A\wedge\neg B)_{3}$. This
validates and the node’s assumptions are updated to $\\{(\neg A)_{1},(\neg
B)_{2}\\}$. The third layer only contains $(\neg A)_{4}$. This validates and
the assumptions are propagated forward. On the fourth layer, the node $B_{6}$
is justified by negation elimination. This validates and the node’s
assumptions are set to $\\{(\neg A)_{1},A_{5}\\}$. The fifth and final layer
only contains the node $B_{9}$. As the node is justified by disjunctive
elimination and is valid, we update the assumptions to $\\{(\neg A)_{1},(A\vee
B)_{8}\\}$. As we have gone through all the layers successfully, the whole
hypergraph is valid.

######  Theorem 1.

For all Proof Graphs $p$ the single-threaded VERIFY$(p)$ is correct with
respect to the validity of the $\mathcal{N\mkern-4.0muD}$ proof corresponding
to $p$.

###### Proof.

An algorithm is correct if it is sound and complete (termination is trivial).
We prove completeness and soundness follows from symmetry. A natural deduction
proof is valid if all steps are valid. For a step to be valid it needs to pass
the _syntactic transformation_ and the _assumption constraints_. From these,
only the assumption constraint check requires information from outside the
node and its parents. The rules of natural deduction in Figure 1 show how
assumptions are computed based on the parent node’s assumption sets. As such,
parents of a node must be verified beforehand and have their assumptions
computed. Nodes that are justified via assumptions mark the base case of this
procedure as their assumption set only contains itself. Due to the definition
of the layering in Equation 1 and its usage in Line 3, assumptions are in the
first layer and the parents of a node must be in the previous layer. This
means that the parents are verified and their assumptions are computed
beforehand on lines 6-9. Inductively this means that all nodes are verified
and have their assumptions computed successfully. Hence, the hypergraph proof
itself is verified. ∎

Layer | Nodes
---|---
0 | 2,4,7,16,
| 23,20,24,18
1 | 5,6,8,9,15,
| 14,21,25,17
2 | 3,11,10, 22
3 | 12,19
4 | 1, 13
5 | 0

Figure 5: (Left) A proof of logical or ($\lor$) distributivity over logical
and ($\land$). (Right) The nodes of the left proof grouped by layer.

###  3.2 Parallel Implementation (Non-optimized Parallel)

Within a layer, each node only depends on nodes in layers prior. This means
that a node on some layer $n$ does not depend on any other node on layer $n$.
For our initial parallel implementation, fully described in Algorithm 2, we
take advantage of this and verify the validity of each node on the same layer
in parallel. In our implementation, we used a shared memory approach. To
combat thread-safety issues we introduce a vector for each given layer called
aIds. This vector lives in shared memory. Each entry holds a set of node ids
and its length is the number of nodes in the current layer. After computing
the layers, each node gets evenly distributed to the available threads. Each
individual thread would then verify the nodes it was assigned and update the
assumptions of the appropriate index within aIds. This is thread-safe because
each entry only gets written to by the thread that its corresponding node id
has been assigned to. The parallel portion of the algorithm additionally
performs an AND reduction on the verification result of each node. This means
that if any result of the individual verifications is false, then the entire
verification result is false. After the parallel portion is finished, the
global assumption map gets updated using aIds.

Let us illustrate the distribution of nodes with the example from Figure 5. In
the graphic, the number at the top of each node represents its identifier. For
brevity, we will use those numbers when referring to the nodes. As the zeroth
layer only contains assumptions that are trivially verifiable, we will start
our discussion from layer one. In this layer, we have the following nodes:

$L(1)=\\{5,6,8,9,15,14,21,25,17\\}$

For the sake of example, let us say we have three threads. Then thread 0 would
be assigned $\\{5,6,8\\}$, thread 1 would be assigned $\\{9,15,14\\}$, and
thread 2 would be assigned $\\{21,25,17\\}$. Let us focus on thread 0. Each of
the three nodes verifies and the following assignments are made to aIds based
on the justification used:

$\displaystyle aIds(5)$ $\displaystyle=\\{assumptions(parent(5))\\}$
$\displaystyle aIds(6)$ $\displaystyle=\\{assumptions(parent(6))\\}$
$\displaystyle aIds(8)$ $\displaystyle=\\{assumptions(parent(8))\\}$

After the parallel portion, the data within aIds are copied into assumptions
as a way to ensure thread-safety. On the next layer, we have the following
nodes: $L(2)=\\{3,11,10,22\\}$. This then gets distributed with thread 0
getting $\\{3,11\\}$, thread 1 obtaining $\\{10\\}$, and thread 2 obtaining
$\\{22\\}$. Focusing on the first thread again, the nodes verify and the
following assignments are made to aIds:

$\displaystyle aIds(3)$ $\displaystyle=\\{assumptions(5),assumptions(6)\\}$
$\displaystyle aIds(11)$ $\displaystyle=\\{assumptions(8)\\}$

Notice that each of the items in those sets contains assumptions that were
computed in the previous layer. They were originally assigned within aIds but
then copied to assumptions. The results of each individual node verification
were stored in NodeValid which is then AND-reduced into the variable
LayerValid. Hence after the end of the parallel portion, the variable
LayerValid would be true unless one of the nodes in the parallel portion
failed to verify.

Algorithm 2 Multi-Threaded Algorithm

1:procedure verify(ProofGraph p)

2: Initialize assumptions to be empty.

3: Create set of nodes on each layer using Equation 1 and store in layerMap.

4: for layerNodes in layerMap do

5: nl = length(layerNodes)

6: aIds = sharedVector(length=nl)

7: LayerValid = true

8: for n in layerNodes in _parallel_ do

9: justification = just(n)

10: ruleInfo = (m, assumptions(m)) $\forall$ m $\in$ parents(n)

11: NodeValid = is_valid(n, justification, ruleInfo)

12: if NodeValid then

13: Update aIds(n) using justification and ruleInfo

14: AND_reduce(LayerValid, NodeValid)

15: if not LayerValid then

16: return false

17: Update assumptions(n) using aIds

18: return true

###  3.3 Multi-Threaded Static Load Balancing Optimization (Load Balancing)

Notice when going over Figure 5 in the last example that the distribution of
nodes in the second layer was uneven. The assignment had one thread verifying
two while the others verifying only a single one. In fact, we can speak to
this more generally. Let $T$ represent the number of threads available and
$l_{i}$ be the number of nodes in layer $i$. Let us assume that the
verification of one node takes two units of work total: one to verify the
syntax and one to verify the assumptions. Let $m=l_{i}\bmod T$. Then, if
$m\neq 0$ there are $(T-m)$ threads that are doing one less unit of work.

Algorithm 3 Multi-Threaded Load Balance Algorithm

1:procedure verify(ProofGraph p)

2: Initialize assumptions to be empty.

3: Create set of nodes on each layer using Equation 1 and store in layerMap.

4: AllNodes = Flatten(layers)

5: numSyntaxVerified = 0

6: for layerNodes in layerMap do

7: nl = length(layerNodes)

8: aIds = sharedVector(length=nl)

9: LayerValid = true

10: layerSyntaxVerified = 0

11: for n in layerNodes in _parallel_ do

12: justification = just(n)

13: ruleInfo = (m, assumptions(m)) $\forall$ m $\in$ parents(n)

14: NodeValid = is_valid(n, ruleInfo)

15: if NodeValid then

16: Update aIds(n) using justification and ruleInfo

17: threadIterSyntaxVerified = 1

18: if thread verifying less nodes then

19: extraN = AllNodes[numSyntaxVerified + threadId]

20: NodeValid = NodeValid and syntaxVerify(extraN, parents(extraN))

21: threadIterSyntaxVerified = 2

22: SUM_reduce(layerSyntaxVerified, threadIterSyntaxVerified)

23: AND_reduce(LayerValid, NodeValid)

24: if not LayerValid then

25: return false

26: Update assumptions(n) using aIds

27: numSyntaxVerified = numSyntaxVerified + layerSyntaxVerified

28: return true

It is with this consideration that we look at static load balancing, presented
in Algorithm 3. For the threads with one less unit of work, they take a node
from a future layer and syntax verify them. This approach is valid because
syntax verification only requires the current node and its parents’ formulae
which are stored in the proof graph and does not require additional
information from the prior layers such as assumption sets. In order to ensure
that the nodes that are syntax verified by the remaining $(T-m)$ threads are
distinct, we make use of another reduction variable numSyntaxVerified. Each
thread would be assigned the node that’s the sum of that variable and its
thread id. Do note that this is different from dynamic load balancing as the
amount of work is evenly distributed and does not take into account during
runtime some threads finishing before others.

Let us turn to our example from Figure 5 again. Recall that the distribution
of work at layer two was the following: thread 0 maps to $\\{3,11\\}$, thread
1 has $\\{10\\}$, and thread 2 has $\\{22\\}$. We can then squeeze in syntax
verification checks in thread 1 and thread 2. Then, the new allocation
becomes: thread 0 maps to $\\{3,11\\}$, thread 1 maps to $\\{10,x_{s}\\}$, and
thread 2 maps to $\\{22,y_{s}\\}$. The subscript denotes how we are only
performing a syntax verification at that step. Recall that we can not perform
full verification of nodes in future layers because we do not know if there’s
a node on the current layer that its assumptions depends on. The question then
is: how are $x_{s}$ and $y_{s}$ calculated? As noted before, this is where we
keep track of the total number of nodes that we have syntax verified already.
If we have a flat vector of all nodes that are partially ordered by their
layer number, then for thread $i$ we can have it syntax verify
$\texttt{numSyntaxVerified}+i$ element of that flat vector. A sum reduction
then keeps track of the total number of syntax verifications performed on a
given layer which is later used to update numSyntaxVerified.

###  3.4 Parallel Distribution of Syntax Checks (Syntax-First)

In the last section we discussed that syntax verification can occur beyond the
current layer being considered. In fact, syntax verification can occur outside
of the layering structure in general which this optimization considers. In
this approach we first perform the syntax verification in parallel over all
nodes before iterating over the layers. This approach is outlined in Algorithm
4. This not only has the benefit of lowering the time to find a syntactic
error, but also more evenly distributes the syntax verification over all
threads.

For our example in Figure 5, the proof graph contains node ids $0$ through
$25$. If we have three threads, then thread $0$ would be assigned nodes $0$
through $8$, thread $1$ would be assigned nodes $9$ through $16$, and thread
$2$ would be assigned nodes $17$ through $25$. Each thread would then loop
over their assigned nodes and syntax verify them. When the three threads
finish, if any of their nodes failed to syntax verify, then the algorithm
would end and the proof graph verification would fail. In this example,
however, the nodes pass the syntax verification. The rest of the algorithm
closely follows Algorithm 2 where instead of performing a full verification,
we only verify that the assumption constraints hold.

Algorithm 4 Multi-Threaded Syntax Check First Algorithm

1:procedure verify(ProofGraph p)

2: syntaxValid = True

3: for n in p.nodes in _parallel_ do

4: valid = verifySyntax(n, parents(n))

5: AND_reduce(syntaxValid, valid)

6: if not syntaxValid then

7: return false

8: Initialize assumptions to be empty.

9: Create set of nodes on each layer using Equation 1 and store in layerMap.

10: for layerNodes in layerMap do

11: nl = length(layerNodes)

12: aIds = sharedVector(length=nl)

13: LayerValid = true

14: for n in layerNodes in _parallel_ do

15: justification = just(n)

16: ruleInfo = (m, assumptions(m)) $\forall$ m $\in$ parents(n)

17: NodeValid = verifyAssumptions(n, justification, ruleInfo)

18: if NodeValid then

19: Update aIds(n) using justification and ruleInfo

20: AND_reduce(LayerValid, NodeValid)

21: if not LayerValid then

22: return false

23: Update assumptions(n) using aids

24: return true

##  4 Methodology and Results

To discuss the performance of our algorithms, we provide an empirical
investigation. To this end, we look toward a comparison of the number of
seconds needed to verify various proof structures using the algorithms
described before. Inspired by the topologies used in computer network design
[3], we introduce a directed variant that we call directed acyclic network
topologies or DANTs. These DANTs represent different classes of possible
proofs with which we perform benchmarks over.

###  4.1 Directed Acyclic Network Topologies (DANTs)

Figure 6: Straight, Parallel-Branch, then Tree Topologies

We have identified three distinct classes of DANTs which we include in our
benchmark of proof graphs for analysis. The pictorial depiction is shown in
Figure 6 and is generated as so: Straight Line $(n)$: Parameterized by the
total number of nodes $n$, this topology only contains one assumption at the
top and then each future inference is a disjunction introduction. This
enforces a straight linear proof with no branching. We do not expect any
speedup in the parallel algorithm in this case as each layer only has one
node. Parallel Branches $(b,n)$: This topology emulates multiple lines of
independent reasoning before combining towards the end. It starts off with $b$
separate assumptions and then performs a disjunctive introduction on each
assumption $n$ times before iteratively applying conjunctive introduction to
each branch until there is one remaining. We expect the number of branches
will correlate with the scalability of verification. It should be noted that
this topology is isomorphic to a straight topology of length $n$ when $b=1$
and emulates a tree like topology of height $b$ when $b>1$. Tree $(h)$: In
this topology we generate $2^{h}$ assumptions and iteratively apply
conjunction introduction $h$ times until we reach a single node. This creates
a balanced binary tree. We hypothesize the greatest amount of speedup from
this topology.

###  4.2 Empirical Analysis

We perform two classes of experiments: (1) a parallel strong scaling study in
which the proof to be verified is held constant while the number of processors
increases; (2) a problem size scaling study in which we hold the number of
threads constant and look at how each method performs as the problem gets
harder.

####  4.2.1 Implementation Details

Our benchmarks were performed on one node of the IBM DCS supercomputer, AiMOS,
at Rensselaer Polytechnic Institute. Our code is available at
https://github.com/RAIRLab/Parallel-Verifier 333For reproducibility of our
results, please see the following link for the specific commit the results of
this paper is based on: https://github.com/RAIRLab/Parallel-
Verifier/tree/a661abbe5bf038a3fa8645b8af532b0a60daebe5. The code is
implemented in C++11 and makes use of the standard C++ library data
structures. For the multiprocessing component, we use the OpenMP library [6].
OpenMP operates over software threads which are assigned to CPUs. We ensure
during our scaling study that the system is not oversubscribed, meaning that
there is just a single thread used per CPU. AiMOS provides us a single node on
which ten physical cores are available; however one is reserved for the
operating system and IO, therefore nine are used for our experiments. For our
benchmarks we do not include the time it took for initialization, file
parsing, or proof parsing; we only measure the time taken to verify the proof.
For this, we record the clock-cycles before and after the execution of the
verification algorithm and use their difference to compute the total cycles.
We then compute the number of seconds taken by each method through dividing
the number of total cycles by the base clock rate of 512MHz.

####  4.2.2 Strong Scaling

For our strong scaling study we vary the number of threads used while holding
the DANT instance constant. For the straight topology, we consider a length
$n$ of 150. For the branch topology, we consider $b=150$ branches each with a
length of $n=100$. Lastly, for the tree topology, we consider $h=16$
conjunction introductions for a total number of $2^{16}$ vertices. Results can
be seen on the left of Figure 7. The strong scaling results show a clear
benefit to our parallelized verification approach. In the case of the straight
topology the serial algorithm vastly outperforms the parallel algorithms,
which is expected as in this topology there is only one node per layer. There
are clear overheads to parallelization, such as waiting for all threads to
finish, that make timing differences visible as the number of threads
increases for the straight topology. For the branch topology with 150 branches
we see that our parallel methods scale well, particularly load balancing which
beats out syntax-first and non-optimized parallel methods. We hypothesize this
is due to the number of remaining nodes on each layer remaining constant which
allows for a good balance of syntax checking vs assumption updating. The
parallel methods perform quite well on the tree topology significantly beating
out the serial method, with non-optimized parallel and syntax-first methods
beating out load balancing likely due to the overhead costs.

####  4.2.3 Problem Scaling

For our problem scaling study we hold the number of threads constant (at
AiMOS’ maximum value of nine) and vary the problem size. For the straight
topology, we consider a chain of disjunctive introductions of lengths ($n$)
100, 150, 200, 250, 300, 350, and 400. For the branch topology, we consider a
fixed branch length of $n=100$ and vary the number of branches ($b$) at 30,
50, 70, 90, 110, 130, and 150. Lastly for the tree topology, we create binary
trees of heights ($h$) 8, 10, 12, 14, 16, 18, and 20. Results can be seen on
the right side of Figure 7. We hypothesize the straight topology scaling is
not linear due to overheads such as the formulae length increasing as the
problem size increases. We see that for all problem sizes on the straight
topology, the serial implementation outperforms the parallel implementation.
This aligns with the observation in the strong scaling study that the parallel
methods have overheads and the fact that for all parallel methods, only one
node is on each layer, preventing the majority of the threads from doing any
work. In the branch topology, the results show that as the number of branches
increases, the effectiveness of parallel methods increases. This is
particularly shown in load balancing, due to the reasons discussed in §4.2.2.
For the tree topology, there is an exponential increase in the time taken as
the problem grows, largely due to the fact that the number of nodes to verify
increases exponentially ($2^{n}$) as the problem size increases. We see that
as the problem size grows, the performance of our parallel methods over the
serial method increases substantially.

Figure 7: (Left) Strong scaling study results (Right) Problem scaling study
results.

##  5 Related Work

Past work has investigated parallel or concurrent verification of other
logical calculi. For example the developers of Isabelle [25], a proof
assistant with support for first-order logic, higher-order logic, and Zermelo-
Fraenkel set theory, used concurrent programming for the efficient
verification of LCF-style proofs [19]. In their work, during the verification
of a proof, if a reference to another proof is made, and that proof has yet to
be verified, then a promise is deferred. At the end of verification, all
promises are resolved and localized errors are then shown to the user [22,
23]. This work operates over entire proofs while we focus on parallelizing
steps within a proof. In [24], Wenzel introduces what he calls granularities
of concurrency within verifying a single proof. The levels include concurrent
verification of theories, concurrent verification of commands, and concurrent
verification of subproofs. In terms of our work, we do not consider extra
background theories, commands correspond to our proof steps, and we do not
consider subproofs in our work. As discussed in §2, there is a definition of a
subproof in our natural deduction hypergraphs. However, it’s not something
specified by the creator of the proof and there can be $n$ different subproofs
for a proof with $n$ nodes.

Färber looked at concurrent verification of commands in his work parallelizing
proof checking inside the lambda-Pi calculus modulo rewriting [9]. In this
work, he breaks up a command into four tasks: parsing, sharing, type
inference, and type checking. Similarly, our work breaks up our inference
rules into two steps: syntactic checks and assumption checks. We additionally
look at the parallel verification of sets of steps or commands, as opposed to
only looking at the concurrency within each command.

##  6 Conclusion

In this work, we presented a layering based algorithm that decouples the
underlying semantic dependencies of proof steps in natural deduction. Through
this, we introduced a suite of new algorithms which use layers to parallelize
verification of hypergraphical natural deduction proofs. Directed acyclic
network topologies (DANTs) were introduced as a benchmark for hypergraphical
proofs and we have shown in our analysis that the parallel algorithms perform
better than their serial counterpart on non-straight DANT instances. These
parallel algorithms were additionally shown to scale through both the strong
scaling and problem scaling studies. This work has applications in formal
verification, specifically in proof assistants.

Our future work falls into four categories: theoretical results, empirical
results, logic extensions, algorithmic optimizations: (1) For theoretical
results, we would benefit from analysis with respect to Amdahl’s Law [12] to
calculate the overall speedup with respect to different parallelizable tasks
in each of the algorithms. (2) For further empirical results, we can test
randomized proof topologies or craft a dataset of common natural deduction
proofs. (3) We wish to extend our verifier to handle different types of
logics, specifically first-order and modal logics. First-order logics are used
heavily within proof assistants, and require the ability to represent and
reason over formulae at the term level, including the need for checking if
variables are free or bound in inference rules. We conjecture that despite
these extra requirements, our layer based parallel approaches would still work
on first-order proof graphs. In order to handle modal logics such as K5, we
would have to adapt the algorithm to include additional bookkeeping required
for several of the inference rules. (4) We would like to explore approaches to
scale beyond a single computer. This involves exploring message-passing
parallelism which is often used in distributed computing.

##### Acknowledgements

This paper was supported in part by a fellowship award under contract
FA9550-21-F-0003 through the National Defense Science and Engineering Graduate
(NDSEG) Fellowship Program, sponsored by the Air Force Research Laboratory
(AFRL), the Office of Naval Research (ONR) and the Army Research Office (ARO).

## References

  * [1]
  * [2] Konstantine Arkoudas & Selmer Bringsjord (2009): _Vivid: A framework for combining diagrammatic and symbolic reasoning_.  Artificial Intelligence 173(15), pp. 1367–1405, 10.1016/j.artint.2009.06.002.
  * [3] B Bicsi (2002): _Network design basics for cabling professionals_.  City: McGraw-Hill Professional, pp. 0885–8950.
  * [4] Selmer Bringsjord (2021): _Intermediate Formal Logic and AI_.
  * [5] Selmer Bringsjord, Naveen Sundar Govindarajulu, Joshua Taylor & Alexander Bringsjord (2022): _Logic: A Modern Approach_.  Motalen.
  * [6] Rohit Chandra, Leo Dagum, Ramesh Menon, David Kohr, Dror Maydan & Jeff McDonald (2001): _Parallel programming in OpenMP_.  Morgan kaufmann.
  * [7] The mathlib Community (2019): _The lean mathematical library_.  Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 10.1145/3372885.3373824.
  * [8] Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest & Clifford Stein (2009): _Introduction to Algorithms_ , 2 edition.  MIT Press.  Available at https://api.semanticscholar.org/CorpusID:60621753.
  * [9] Michael Färber (2022): _Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting_.  Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, 10.1145/3497775.3503683.
  * [10] Frederic Brenton Fitch (1953): _Symbolic Logic, An Introduction_.  American Journal of Physics 21, pp. 237–237, 10.2307/2020641.
  * [11] Gerhard Gentzen (1935): _Untersuchungen über das logische Schließen. I_.  Mathematische Zeitschrift 39, pp. 176–210, 10.1007/bf01201353.
  * [12] Mark D. Hill & Michael R. Marty (2008): _Amdahl’s Law in the Multicore Era_.  IEEE Computer 41, pp. 33–38, 10.1109/MC.2008.209.
  * [13] Stanisław Jaśkowski (1934): _On the rules of suppositions in formal logic_.  Studia Logica.
  * [14] Vipin Kumar, Ananth Y. Grama, Anshul Gupta & George Karypis (1994): _Introduction to parallel computing: design and analysis of algorithms_.  Benjamin-Cummings Publishing Co., Inc.
  * [15] Leonardo de Moura & Sebastian Ullrich (2021): _The Lean 4 Theorem Prover and Programming Language_.  In: International Conference on Automated Deduction, Springer, pp. 625–635, 10.1007/978-3-030-79876-5_37.
  * [16] James Oswald & Brandon Rozek (2022): _Lazyslate_.  Available at https://github.com/James-Oswald/lazyslate.
  * [17] Francis Jeffry Pelletier & Allen Hazen (2023): _Natural Deduction Systems in Logic_.  In Edward N. Zalta & Uri Nodelman, editors: The Stanford Encyclopedia of Philosophy, Spring 2023 edition, Metaphysics Research Lab, Stanford University, pp. 1–1.
  * [18] Dag Prawitz (1965): _Natural Deduction: A Proof-Theoretical Study_.  Dover Publications, 10.2307/2271676.
  * [19] Dana S Scott (1993): _A type-theoretical alternative to ISWIM, CUCH, OWHY_.  Theoretical Computer Science 121(1-2), pp. 411–440, 10.1016/0304-3975(93)90095-B.
  * [20] The Coq Development Team (2019): _The Coq Proof Assistant_ , 10.5281/zenodo.3476303.
  * [21] Vitaly I. Voloshin (2013): _Introduction to Graph and Hypergraph Theory_.  Nova Kroshka Books.
  * [22] Makarius Wenzel (2009): _Parallel Proof Checking in Isabelle/Isar_.
  * [23] Makarius Wenzel (2013): _READ-EVAL-PRINT in parallel and asynchronous proof-checking_.  arXiv preprint arXiv:1307.1944, 10.4204/eptcs.118.4.
  * [24] Makarius Wenzel (2013): _Shared-Memory Multiprocessing for Interactive Theorem Proving_.  In Sandrine Blazy, Christine Paulin-Mohring & David Pichardie, editors: Interactive Theorem Proving, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 418–434, 10.1007/978-3-642-39634-2_30.
  * [25] Makarius Wenzel, Lawrence C Paulson & Tobias Nipkow (2008): _The isabelle framework_.  In: International Conference on Theorem Proving in Higher Order Logics, Springer, pp. 33–38, 10.1007/978-3-540-71067-7_7.