dataesr/scientific-paragraphs-categorization huggingface dataset:
The dynamic parameter is an expression of max and min functions of the outer loop iterator and an array of constants. We derive the static upper bound parameter u from the BLOCK_SIZE constant, a global parameter of the program to declare the size of an image block. Since we target a GPU architecture, we ought to extract large degrees of parallelism from multiple nested loops. As explained in subsection 4. 5, we sink the definition statements of dynamic parameters within inner dynamic counted loops and apply our AST generation scheme for a combined band for GPU architecture. We may then generate the CUDA code with parameter values for tile sizes, block sizes, grid sizes, etc. We show performance results with and without host-device data transfer time, in Figure  10 , considering multiple block sizes.
It makes their approach effective when most rows have a similar number of non-zeros. Our technique implements a similar idea without data transformation by extending the upper bound of the inner dynamic counted loop to the maximum number of non-zeros, and automatically emitting early exit statements when there are fewer non-zeros in a row, minimizing the number of iterations of the dynamic counted loop. The performance is shown in Figure  13  together with that of the CUSP library. A format_conversion exception is captured when experimenting the CUSP library with mac_econ_fwd500, mc2depi, pwtk and tomographic1 while our technique remains applicable on all formats. Although the manually-tuned library outperforms the proposed technique under three inputs, our method performs better in general.
In addition, our technique provides comparable or higher performance than the inspector/executor scheme without the associated overhead. The inspector/executor strategy used in  [24]  obtains performance gains by optimizing the data layout. Our technique can also apply to the executor of this strategy as a complementary optimization, further improving the performance of the executor. The inspector/executor strategy, however, is not so satisfying as expected for CSR, since the CSR executor is roughly the same with the original code. As a result, the performance of our generated code when applying our technique on the CSR executor is also roughly the same with that applying on the orignal code, as shown in Figure  12. As a complementary optimization, our technique can speedup the CSR executor by up to 4.
Performance on CPU Architectures We also evaluate our technique on CPU architectures. Unlike generating CUDA code, the original dynamic condition can be taken back when generating OpenMP code on CPU architectures, avoiding the combination of nested bands and the refactoring of the control flow. The performance results are shown in Figures  14 15 16 17. We do not show the performance of dynamic programming examples on CPU architectures since our code generation scheme generates OpenMP code identical with the hand written one. For the remaining benchmarks, our technique enables aggressive loop transformations including tiling, interchange, etc. , leading to a better performance when these optimizations are turned on. As the CUSP library is designed for GPU architectures, we only compare the performance of the SpMV code with Venkat et al.
Parallelism is exposed at the expense of an invalid space-time mapping that needs to be corrected at run time. Beyond polyhedral techniques, Rauchwerge  [21]  proposed a speculative code transformation and hybrid static-dynamic parallelization method for while loops. An alternative, conservative technique, consists in enumerating a super-set of the target execution space  [12] [13] [14] [15] , and then eliminating invalid iterations by determining termination detection on the fly. The authors present solutions for both distributed and shared memory architectures. Benabderrahmane et al. [5]  introduce a general framework to parallelize and optimize arbitrary while loops by modeling controlflow predicates. They transform a while loop as a for loop iterating from 0 to +∞. Compared to these approaches to parallelizing while loops in the polyhedral model, our technique relies on systems of affine inequalities only, as implemented in state-of-the-art polyhedral libraries.
Conclusion In this paper, we studied the parallelizing compilation and optimization of an important class of loop nests where counted loops have a dynamically computed, data-dependent upper bound. Such loops are amenable to a wider set of transformations than general while loops. To achieve this, we introduce a static upper bound and model control dependences on datadependent predicates by revisiting a state-of-the-art framework to parallelize arbitrary while loops. We specialize this framework to facilitate its integration in schedule-tree-based affine scheduling and code generation algorithms, covering all scenarios from a single dynamic counted loop to nested parallelism across bands mapped to GPUs with fixed-size data-parallel grids. Our method relies on systems of affine inequalities, as implemented in state-of-the-art polyhedral libraries.
Recent advances in the field of electron cryomicroscopy (cryo-EM) have resulted in a rapidly increasing number of atomic models of biomacromolecules that have been solved using this technique and deposited in the Protein Data Bank and the Electron Microscopy Data Bank. Similar to macromolecular crystallography, validation tools for these models and maps are required. While some of these validation tools may be borrowed from crystallography, new methods specifically designed for cryo-EM validation are required. Here, new computational methods and tools implemented in PHENIX are discussed, including d 99 to estimate resolution, phenix. auto_sharpen to improve maps and phenix. mtriage to analyze cryo-EM maps. It is suggested that cryo-EM half-maps and masks should be deposited to facilitate the evaluation and validation of cryo-EM-derived atomic models and maps.
Thus, an overall quality assessment of these models may be useful  (Henderson et al. , 2012; Pintilie et al. , 2016; Joseph et al. , 2017; Neumann et al. , 2018). Here, we survey cryo-EM maps and derived models as well as discuss tools and methods implemented in the PHENIX suite of programs  (Adams et al. , 2010)  specifically designed to evaluate cryo-EM-derived atomic models and maps. We have used these tools to provide an assessment of the quality of a high-resolution subset (4. 5 A ˚or better) of cryo-EM-derived atomic models that are currently available in the Protein Data Bank (PDB;  Bernstein et al. , 1977; Berman et al. , 2000)  and the corresponding maps available in the Electron Microscopy Data Bank (EMDB;  Lawson et al. , 2011). The analysis shows an improvement in model quality in recent years, while also suggesting that there are opportunities for further improvement that will require the development of new validation tools and procedures.
Extraction of atomic models and maps from the PDB and EMDB Atomic models and maps were automatically extracted from the PDB and the EMDB, respectively, to provide matching pairs  (model, map). A Python script based on cctbx (Grosse-Kunstleve &  Adams, 2002)  was written for this purpose. Entries were rejected if any of the items below were true. (i) The box information (for example, the CRYST1 record in the PDB coordinate file) was impossible to interpret unambiguously considering both the model file and the data associated with the map file. (ii) MTRIX or BIOMT matrices are present but cannot be extracted owing to syntactical errors in the records, or the corresponding matrices do not satisfy the numerical requirements for rotation matrices. (iii) The model or map contains errors such as a C atom in a Gly residue.
Tools All calculations were performed fully automatically, with no manual intervention, and therefore can be routinely repeated. Tools available in PHENIX [MolProbity  (Chen et al. , 2010)  and EM-Ringer  (Barad et al. , 2015) ] were used to calculate various statistics such as Ramachandran plots, residue sidechain rotamer outliers and model-map correlations. The cctbx software library was used to extract files from databases and to compute, process and accumulate statistics. Some new tools were developed to address specific tasks (for example, phenix. mtriage to analyze cryo-EM maps). All scripts used in this work are publicly available (http://phenix-online. org/ phenix_data/afonine/cryoem_validation/). PyMOL  (DeLano, 2002)  and UCSF Chimera  (Goddard et al. , 2018)  were used for molecular graphics.
An example of a Ramachandran plot outlier that in fact is valid can be found in isocyanide hydratase (PDB entry 3NoQ 2 ;  Lakshminarasimhan et al. , 2010). A valid outlier must be supported by the experimental data (unambiguously resolved in the map, for instance) and be justified by local chemistry (for example, a strained conformation stabilized by hydrogen bonding). The overall data resolution is neither the only nor the most important resolving factor of the data. Other factors, such as data completeness in crystallography or local variations of resolution in cryo-EM, may be equally important. With this in mind, it will be increasingly unlikely that outliers can be supported by the experimental data as the resolution worsens. In most cases we would expect that a model refined against data at a resolution of $3 A ˚or worse would have very few or no justifiable geometric outliers.
5a ). However, this is not the case when the structure contains mixtures of well and less well defined parts; an example is PDB entry 3JBS. 3 Therefore, the CC volume and CC mask values and the difference between them may be indicative of a variability in model quality within a structure. As opposed to CC mask and CC volume , two other coefficients, CC box and CC peaks , quantify the fit of a given model against the entire map and both indicate the presence of non-interpreted parts of the map. An advantage of CC peaks over CC box is its independence of box size, while CC box depends on the size of the box. Calculation of CC box includes the comparison of two relatively flat regions outside the structure that artificially results in larger values, CC box ! CC peaks, for all models (Fig. 5b ).
An alternative hypothesis is an incomplete optimization of the model parameters (coordinates, occupancies of ADPs) with respect to the map. Indeed, as discussed below in x3. 4, we find that about 31% of all models examined possess unrealistic occupancy or/and ADP values, such as all being set to zero or other unlikely values. Given that occupancies and ADPs are used to calculate the model maps (see x2. 1. 1), it is not surprising to find low CC values for such models. Figs. 6, 7 and 8 serve as examples of cases in which incomplete optimization can result in low model-to-map correlation and show that rather simple refinement can address some of the issues (Figs. 7  and 8 ). Finally, some extremely low model-map correlations (e. g. CC < 0. 1; Fig. 4a ) can be explained by origin mismatch between the map and model (for example, PDB entry 3A5X and EMDB entry 1641).
Note that the best correlation CC(d FSC , d FSC_model ) is achieved for d FSC_model calculated at FSC = 0. 143. We note that this resolution metric is rather insensitive to the masking of the map (Fig. 9f ). The   9g ) but it is rather insensitive to masking (Fig. 9h ). 3. 6. 4. Analysis of selected examples with a large discrepancy between d FSC , d 99 and d model. Several examples below illustrate the utility and limitations of the resolution-estimation methods described in this manuscript (Table  1 ). We show that the differences between the various measures of resolution may originate from: (i) particular properties of the model and/or the data (map), (ii) annotation or some other procedural errors and (iii) limitations of the resolution metrics used. Cystic fibrosis transmembrane conductance regulator (CFTR).
The reported resolution for CFTR  (Zhang & Chen, 2016 ; PDB entry 5UAR; EMDB map code 8461) is d FSC = 3. 7 A ˚. Visual inspection of the map suggests a significantly lower resolution (Fig. 10 ), which agrees with the model-based estimate of resolution d model = 6. 7 A ˚. At the same time d 99 = 1. 9 A ˚suggests that Fourier coefficients well beyond d FSC are significant enough to affect the appearance of the map. The value of d FSC_model calculated at FSC = 0 ranges between 3. 3 and 3. 6 A ˚(depending on whether sharpening or masking were used), suggesting that there is at least some correlation between modelderived and experimental maps up to this resolution. The original publication Scatter plots showing the relationship between the different resolution estimates and their different ways of calculation.
9-1 A ˚map makes the map deteriorate (Fig. 11b ; B = À20 A ˚2). Maltose-binding protein genetically fused to dodecameric glutamine synthetase. In this example  (Coscia et al. , 2016 ; PDB entry 5LDF; EMDB map code 4039), the map shows details specific for a resolution higher than the reported d FSC = 6. 2 A ˚. For example, a large number of side chains can be well distinguished (Fig. 12 ). Indeed, both suggested metrics give higher values: d model = 4. 0 A ˚, d 99 = 4. 4 A ˚. This means that for this structure Fourier coefficients of a resolution higher than d FSC = 6. 2 A ˚cannot be neglected. Indeed, the relevant article mentions that the resolution of the final reconstruction was 4. 2 A ˚, in agreement with our calculations, and the local resolution varies between 10 and 3 A ˚, with the bestresolved regions being in the middle of the molecule (Fig.
12b ). Glutamate dehydrogenase. For this example  (Merk et al. , 2016 ; PDB entry 5K12; EMDB map code 8194), d FSC = 1. 8 A ˚and d 99 = 1. 9 A ˚, while d model = 3. 0 A ˚. This shows that even when Fourier coefficients are present up to a resolution of 1. 8 A ˚and accurately defined, their contribution is relatively weak in comparison with other coefficients and the map appears more consistent with 3. 0 A ˚resolution. Indeed, maps calculated using Fourier map coefficients in the ranges 1. 8-1 and 3-1 A ˚appear essentially the same (Figs. 13a  and 13b ). Furthermore, the overall (CC box ) and peak (CC peak )  (Urzhumtsev et al. , 2014)  correlations between these two maps are 0. 96 and 0. 86, respectively. For the model-calculated maps at 1. 8 and 3 A ˚resolution these correlations are 0. 88 and 0.
40, respectively. This indicates that eliminating the 1. 8-3 A ˚resolution range from the map coefficients has little effect on the original map. The resolution d FSC_model obtained at FSC = 0, 0. 143 and 0. 5 is 1. 8, 2. 3 and 3 A ˚, respectively, which confirms that there is some signal in this range but it is just weak. A sharpened map at 1. 8-1 A ˚(Fig. 13c ) shows details expected at resolutions around 2 A ˚, and truncating the data to 2. 3-1 A does change the map visibly (Fig. 13d ). We note that not all regions of the volume behave similarly to as in this example (Fig. 13 ) because the resolution varies across the volume, with 1. 8 A ˚resolution for the best parts. This explains the small difference in the correlations calculated between 1. 8 and 3. 0 A fltered maps. 3. 4 † The original map for PDB entry 5UAR contains high-resolution features (likely to be noise) outside the model.
These features can be removed by masking (compare d 99 for the masked and unmasked maps). The unsharpened map does not show higher resolution details (see d model ). The model reproduces all details up to d FSC (compare d FSC and d FSC_model ). High-resolution filtering followed by sharpening may be required to build and confirm these details. ‡ The original map for PDB entry 5LDF contains details of a resolution higher than d FSC (compare d FSC and d 99 ); the molecular region also contains these details (compare d 99 for the masked and unmasked maps). The unsharpened map indeed looks like a map nearer 6 A ˚resolution (the difference between d model calculated with underestimated B = 0 and overestimated B = 220 A ˚2). The model reproduces details up to a resolution slightly higher than 4 A ˚(see d FSC_model ), which is confirmed by all metrics calculated for the sharpened map.
It is possible that d FSC is underestimated. § The original map for PDB entry 5K12 contains high-resolution details up to d FSC (d 99 for the unmasked map). Inside the molecular region neither the original nor the sharpened map show such details (d 99 for masked maps) and the map itself looks like a 3 A ˚resolution map (see d model ). At the same time, the model reproduces the data up to a resolution near d FSC (d FSC_model ). To visualize these details, the default sharpening is insufficient and omitting dominating lower resolution data may be needed. } The original data for PDB entry 5K7L are weak at higher resolution and the original map shows limited detail (low d 99 for unsharpened maps); these details do appear in the sharpened map (compare d 99 and d FSC , also compare d 99 for sharpened and unsharpened maps).
Indeed, the original map in the molecular region is blurred by very large B   Voltage-gated K + channel Eag1. This is a case (PDB entry 5K7L; EMDB map code 8215;  Whicher & MacKinnon, 2016)  in which the resolutions reported in the map (d FSC ) and estimated using the model (d model ) match at a value of 3. 8 A ˚, while d 99 = 7. 4 A ˚. Performing similar calculations as those carried out for CFTR above, we find that the original map (Fig. 14a ) and the map calculated using a resolution range of 7. 4-1 A ˚(Fig. 14b ) appear to be essentially the same except for small hints of side chains in the higher resolution map. Inspecting the original map at lower contour levels does not reveal any more information for the side chains. Calculating a map using the 3. 8-7. 4 A ˚resolution range results in a map that is expectedly noisy overall but also clearly shows side chains for many residues (Fig.
Conclusions Crystallography and cryo-EM are similar in the sense that both yield an experimental three-dimensional map to be interpreted in terms of a three-dimensional atomic model. In crystallography the experimental data are diffraction intensities, and in cryo-EM the data are three-dimensional objects reconstructed from two-dimensional projections acquired from the microscope. Once an initial map (Fourier image of electron or nuclear density distribution in crystallography) or three-dimensional reconstruction (image of electrostatic potential in cryo-EM) is obtained, the next steps leading to the final refined atomic model are very similar. Integral to these steps is validation of the data, the atomic model and the fit of the atomic model to the data. However, since the types of experimental data are different, the two methods require different validation approaches.
We envisage a Summary Table  similar  to the widely accepted crystallographic 'Table  1 ', which would include information about the highest resolution shell of a Fourier space, including FSC for half-maps, FSC map-model and relative strength of amplitudes in comparison to other resolution shells. Some other metrics, for example those discussed in  Tickle (2012) , can also be included. There is an opportunity to address some of the current limitations in the validation of cryo-EM maps and the models derived from them before the database grows significantly in size. Improvements in the deposition process would minimize some of the inconsistences in models and maps that we have observed. Cryo-EM reconstructions have reached a resolution that warrants rigorous checks on coordinates, atomic displacement parameters and atomic occupancies.
Funding information This work was supported by the  NIH  (grant  GM063210  to PDA and TT) and the  PHENIX Industrial Consortium. This work was supported in part by the  US Department of Energy  under Contract No. DE-AC02-05CH11231. BK and AU thank the  Centre National de la Recherche Scientifique (CNRS) ,  Association pour la Recherche sur le Cancer (ARC) ,  Institut National du Cancer (INCa) ,  Agence National pour la Recherche (ANR)  and the  French Infrastructure for Integrated Structural Biology (FRISBI)   ANR-10-INSB-05-01  and Instruct, which is part of the  European Strategy Forum on Research Infrastructures (ESFRI).
Reported at resolution d FSC = 2. 9 A ˚, the coefficients are CC volume = 0. 62 and CC mask = 0. 75; other examples are PDB entry 5K0U (d FSC = 2. 8 A ˚; CC volume = 0. 69, CC mask = 0. 84) and PDB entry 5AC9 (d FSC = 3. 2 A ˚; CC volume = 0. 73, CC mask = 0. 89).
Fuel Control System Model This model uses only the ODEs to implement the dynamics. RCRS comes with a publicly available toolset, the RCRS toolset (Fig. 1 ), which consists of: -A full implementation of RCRS in the Isabelle proof assistant  [9]. -A set of analysis procedures for RCRS components, implemented on top of Isabelle and collectively called the Analyzer. An extended version of this paper contains an additional six-page appendix describing a demo of the RCRS toolset  [6]. The extended paper can also be found in a figshare repository  [7]. The figshare repository contains all data (code and models) required to reproduce all results of this paper as well as of  [6] : see Section 7 for more details. The RCRS toolset can be downloaded also from the RCRS web page: http://rcrs. cs. aalto.
e. , non-deterministic systems). Using the former instead of the latter to describe deterministic systems aids the Analyzer to perform simplifications -see Section 5. Theory SimplifyRCRS. thy (2175 lines) implements several of the Analyzer's procedures. In particular, it contains a simplification procedure which reduces composite RCRS components into atomic ones (see Section 5). In addition to the above, there are several theories containing a proof of correctness of our block-diagram translation strategies (see Section 4 and  [10] ), dealing with Simulink types  [12] , generating Python simulation code, and many more. A detailed description of all these theories and graphs depicting their dependencies is included in the documentation of the toolset. The syntax of RCRS components is implemented in Isabelle using a shallow embedding  [2].
The Translator The Translator, called simulink2isabelle, translates hierarchical block diagrams (HBDs), and in particular Simulink models, into RCRS theories  [5]. The Translator (implemented in about 7100 lines of Python code) takes as input a Simulink model (. slx file) and a list of options and generates as output an Isabelle theory (. thy file). The output file contains: (1) the definition of all instances of basic blocks in the Simulink diagram (e. g. , all Adders, Integrators, Constants, etc. ) as atomic RCRS components; (2) the bottom-up definition of all subdiagrams as composite RCRS components; (3) calls to simplification procedures; and (4) theorems stating that the resulting simplified components are equivalent to the original ones. The. thy file may also contain additional content depending on user options as explained below.
Data Availability Statement All results mentioned in this paper as well as in the extended version of this paper  [6]  are fully reproducible using the code, data, and instructions available in the figshare repository: https://doi. org/10. 6084/m9. figshare. 5900911. The figshare repository contains the full implementation of the RCRS toolset, including the formalization of RCRS in Isabelle, the Analyzer, the RCRS Simulink library, and the Translator. The figshare repository also contains sample Simulink We downloaded the Simulink models from https://cps-vo. org/group/ARCH/ benchmarks. One of those models is made available in the figshare repository  [7]  -see also Section 7. We next define three RCRS components (Fig. 5a ): SqrRoot (modeling the square root function, see Section 2), Const1 (modeling the constant 1), and the composite component Syst1, formed by composing Const1 and SqrRoot in series.