dataesr/scientific-paragraphs-categorization huggingface dataset:
Notably, we show here the perfect concordance of the 3 molecular clusters of pulmonary carcinoids independently identified in  [7]  and  [8] , validating the discoveries made by these 2 studies and proving the usefulness of this integrative approach. However, even when primary genomic data are available, barriers to accessing the data still exist, often limiting reuse by the community  [53]. In particular, downloading and re-reprocessing large raw sequencing datasets requires dedicated infrastructure and bioinformatics skills. Indeed, to minimize batch effects when integrating data from different studies, one needs to process it in exactly the same way (e. g. , with the same versions of the same software, the same reference genome, the same annotation databases). As more and more data are generated, the previously mentioned reprocessing will become untenable and replicating these efforts for each new study in each research group represents a waste of resources.
Standardization of laboratory and computational protocols might become a reality when large national medical genomics initiatives become fully operational  [54]. In the meantime there is a need for better data sharing strategies than the traditional "supplementary spreadsheet/raw data" combination that can accelerate the translational impact of molecular findings. One step in this direction is the generation of so-called "tumor maps," which provide an interactive way to explore the molecular data and allow easy statistical interrogation, including generating new hypotheses, but also projecting data from future studies including fewer samples  [13]. This integration method has some limitations though. A fixed reference map could be of interest for easier biological interpretations, but the overall sample size of the datasets used to build the pan-LNEN map remains relatively small.
Thus, the map probably does not capture the complete molecular diversity of the LNENs, and integrating new samples will influence the map and potentially change the clusters obtained after dimensionality reduction. Also, if the harmonization of the new dataset to integrate is not enough to correct for strong batch effects, the interpretation of the projections would be erroneous. Another approach would be to project the new samples into a fixed reference map. However, the stochastic nature of UMAP embedding and its sensitivity to parameter tuning can lead to unstable projection results; thus this task is for now not straightforward and requires further development  [55]. In the meantime, favoring the integration of datasets will, over the years, yield the constitution of molecular maps that will probably be more and more accurate and more adapted to the projection of new samples.
Conclusion Here we provide a molecular map based on homogenized transcriptomic data available for the 4 types of LNENs from 6 different studies. We show that this map represents well both the local and global structure of the data and captures the main biological features previously reported. We provide a full spectrum of data and tools to maximize reuse potential for a wide range of users: raw sequencing reads, gene expression matrix, bioinformatics pipelines, interactive computational notebooks, and an interactive TumorMap. In particular, we indicate how one can update the molecular map by integrating new samples starting from raw sequencing reads. Considering the small sample sizes of molecular studies on rare LNENs, promoting data integration will empower more reliable statistical testing, and this map will therefore serve as a reference in future studies.
Acknowledgments This study is part of the lungNENomics project and the  Rare Cancers Genomics initiative  (http://rarecancersgenomics. com). We also acknowledge the  Cologne Centre for Genomics (Cologne, Germany ) and the  Centre National de Recherche en G énomique Humaine (Evry, France)  for generating high-quality sequencing data. We also thank  Cyrille Cuenin  and  Zdenko Herceg  from the  Epigenetics group at IARC ; and  Teresa Swatloski  and  Josh Stuart  from  UCSC  for their assistance in hosting our map on the UCSC tumormap portal.
Funding This work has been funded by the  US National Institutes of Health  ( NIH R03CA195253  to L. F. C. and J. D. M. ), the  French National Cancer Institute (INCa ,  PRT-K-17-047  to L. F. C. and M. F. ), the  Ligue Nationale contre le Cancer  ( LNCC 2016  to L. F. C. ),  France Genomique  (to J. D. M. ), and the  Neuroendocrine Tumor Research Foundation  (NETRF, Investigator Award 2019 to L. F. C. ). L. M. has a fellowship from the  LNCC.
This is, of course, exactly the security-critical computing base, currently trusted but not trustworthy, that is especially in need of verification -which requires a precise and well-validated definition of the architectural abstraction. Previous work has scarcely touched on this: none of seL4  [27] , CertiKOS  [24, 23] , Komodo  [16] , or  [25, 12] , address realistic architecture concurrency, and they use (at best) idealised models of the sequential systems architecture. The CakeML  [51, 28]  and CompCert  [29]  verified compilers target only sequential user-mode ISA fragments. In this paper we focus on one aspect of system semantics: instruction fetch and cache maintenance, for ARMv8-A. The ability to execute code that has previously been written to data memory is fundamental to computing: finegrained self-modifying code is now rare, and (rightly) deprecated, but program loading, dynamic linking, JIT compilation, debugging, and OS configuration all rely on executing code from data writes.
However, because these are relatively infrequent operations, hardware designers have been able to optimise by partially separating the instruction and data paths, e. g. with distinct instruction caching, which by default may not be coherent with data accesses. This can introduce programmer-visible behaviour analogous to that of user-mode relaxed-memory concurrency, and require specific additional synchronisation to correctly pick up code modifications. Exactly what these are is not entirely clear in the current ARMv8-A architecture text, just as pre-2018 user-mode concurrency was not. Our main contribution is to clarify this situation, developing precise abstractions that bring the instruction-fetch part of ARMv8-A system behaviour into the domain of rigorous semantics. Arm have stated [private communication] that they intend to incorporate a version of this into their architecture.
We aim thereby to enable future work on system software verification using the techniques of programming languages research: program analysis, model-checking, program logics, etc. We begin ( §2) by recalling the informal architectural guarantees that Arm provide, and the ways in which real-world software systems such as Linux, JavaScript, and WebAssembly change instruction memory. Then: (1) We explore the fundamental phenomena and architecture design questions with a series of examples ( §3). We explore the interactions between instruction fetching, cache maintenance and the 'usual' relaxed memory stores and loads, showing that instruction fetches are more relaxed, and how even fundamental coherence guarantees for data memory do not apply to instruction fetches. Most of these questions arose during the development of our models, in detailed ongoing discussion with the Arm Chief Architect and other Arm staff.
They include questions of several different kinds. Six are clear from the Arm prose specification. Of the others: two are not implied by the prose but are natural choices; five involved substantive new choices by Arm that had not previously been considered and/or documented; for two, either choice could be reasonable, and Arm chose the simpler (and weaker) option; and for one, Arm were independently already strengthening the architecture to accommodate existing software. (2) We give an operational semantics for Arm instruction fetch and icache maintenance ( §4). This is in an abstract-microarchitectural style that supports an operational intuition for how hardware actually works, while abstracting from the mass of detail and the microarchitectural variation of actual hardware implementations.
4. The second DSB ISH ensures the invalidation completes. 5. The final ISB flushes this core's pipeline, forcing a re-fetch of all programorder-later instructions. Some hardware implementations provide extra guarantees, rendering the DC or IC instructions unnecessary. Arm allow software to discover this in an architectural way, by reading the CTR _ EL0 register's DIC and IDC bits. Our modelling handles this, but for brevity we only discuss the weakest case, with CTR _ EL0. DIC=CTR _ EL0. IDC=0, that requires full cache maintenance. Arm make clear that instructions can be prefetched (perhaps speculatively): "How far ahead of the current point of execution instructions are fetched from is IMPLEMENTATION DEFINED. Such prefetching can be either a fixed or a dynamically varying number of instructions, and can follow any or all possible future execution paths.
All this gives some guidance for programmers, but it leaves the exact semantics of instruction fetch and those cache maintenance instructions unclear, and in practice software typically does not use the above sequence verbatim. For example, it may synchronise a range of addresses at once, looping the DC and IC parts, or the final ISB may be subsumed by instruction synchronisation from exception entry or return. Linux has many places where it modifies code at runtime: in boot-time patching of alternatives, modifying kernel code to specialise it to the particular hardware being run on; when the kernel loads code (e. g. when the user calls dl _ open); and in the ptrace system call, used e. g. by the GDB debugger to patch arbitrary instructions with breakpoints at runtime. In Google's Chrome web browser, its WebAssembly and JavaScript just-in-time (JIT) compilers are required to both write new code during execution and modify existing code at runtime.
In JavaScript, this modification happens inside a single thread and so is quite straightforward. The WebAssembly case is more complex, as one thread is modifying the code of another. A software thread can also be moved (by the OS or hypervisor) from one hardware thread to another, perhaps while it is in the middle of some instruction cache maintenance. Moreover, for security reasoning, we have to be able to bound the possible behaviour of arbitrary code. All this means that we cannot treat the above sequence as a whole, as an opaque black box. Instead, we need a precise semantics for each individual instruction, but the existing prose documentation does not provide that. The problem we face is to give such a semantics, that correctly defines behaviour in arbitrary concurrent contexts, that captures the Arm architectural intent, that is strong enough for software, and that abstracts from the variety of hardware implementations (e.
Edges from the initial state are drawn from a small circle. Since we do not modify the code of most locations, we usually omit the fetch events for those instructions, showing only a subgraph of the interesting events, e. g. as on the right above. For Arm, this execution is both architecturally allowed and experimentally observed. Here, and in future tests, we assume some common code consisting of a function at address f which always has the same shape: a branch that might be overwritten, which selects a block that writes a value to register X10 before returning. This is sometimes duplicated at different addresses (f1, f2,. ) or extended to g, with three cases. We sometimes elide the common code. Data-to-Instruction Coherence Fetching from a particular write does imply that program-order-later reads from the same address will see that write (or a coherence successor thereof).
CoFR AArch64 Forbidden: 1:X0=2, 1:X1="B l0" write f=B l1 a: Thread 0 fetch f=B l1 b: fetch LDR X1,[X2] c: read f=B l0 d: Thread 1 irf fpo fe rf This is not clear in the existing prose specification, but the architectural intent that emerged during discussion with Arm is that the given execution should be forbidden, reflecting microarchitectural choices that (1) instructions decode in order, so the fetch b must occur before the read d, and (2) fetches that miss in the instruction cache must read from data storage, so the instruction cache cannot be ahead of the available data. This ensures that fetching from a write means that all threads are now guaranteed to read from that write (or another coherence-after it). Instruction-to-Data Coherence In the other direction, reading from a particular write to some location does not imply that later fetches of that location will see that write (or a coherence successor), as in the following CoRF+ctrl-isb.
MP. FF+dmb+fpo AArch64 Allowed: Without the full cachesync sequence on Thread 0, this is an allowed outcome. Interestingly, adding the cachesync sequence to Thread 0 (Test MP. FF+cachesync+fpo, not shown) is sufficient to make the outcome forbidden, without an ISB in Thread 1, as the cachesync sequence is intended to make it appear that fetches occur in program order. Microarchitecturally, that could be ensured in two ways: either by actually fetching in-order, or by making the IC instruction not only invalidate all the instruction caches (for this address) but also clean any core's pre-fetch buffer stale entries (for this address). Architecturally, this is not clear in the current prose, but, concurrent with this work, Arm were independently strengthening their definition to make it so.
FOW AArch64 Allowed: This is not clear in the existing architecture text. It is a case where the architecture design is not very constrained. On the one hand, it has not been observed, and it is thought unlikely that hardware will ever exhibit this behaviour: it would require keeping multiple writes in the coherent part of the data caches, rather than a single dirty line, which would require more complex cache coherence protocols. On the other hand, there does not seem to be any benefit to software from forbidding it. Arm therefore prefer the choice that gives a simpler and weaker model (here the two happen to coincide), to make it easier to understand and to provide more flexibility for future microarchitectural optimisations. We therefore design our models to allow the above behaviour.
The instruction cache can contain many possible writes for each location ( §3. 6), and it can be spontaneously updated with new writes in the system at any time  ([9, B2. 4. 4] ). To manage IC instructions, each thread keeps a list of addresses yet to be invalidated by in-flight ICs. Data Cache (global) Above the single shared flat memory for the entire system, which sufficed for the multi-copy-atomic ARMv8-A data memory, we insert a shared buffer which is just a list of writes; abstracting from the many possible coherent data cache hierarchies. Data reads must be coherent, reading from the most recent write to the same address in the buffer, but instruction fetches are allowed to read from any such write in the buffer ( §3. 2). Transitions To accommodate instruction fetch and cache maintenance, we introduce new transitions: Fetch Request, Fetch Instruction, Fetch Instruction (Unpredictable), Fetch Instruction (B.
This pushes any write that might have been in the abstract data cache into memory. Now the first DSB's Commit DSB can be taken, allowing Begin IC to happen. This creates entries for each thread, which are discharged by each Propagate IC to Thread (see above). Once all entries are invalidated, a Complete IC can happen. Now, if any thread decodes an instruction for that address, it must have been fetched from the write the DC pushed, or something coherence-after it. If the software thread performing this sequence is interrupted and migrated (by the OS) to a different hardware thread, then, so long as the OS includes the DSB to maintain the thread-local DC ordering, the DC will push the write in an identical way, since it only affects the global abstract data cache. The IC transitions can all be taken, and the sequence continues as before, just on a new hardware thread.
The relations are: program order (po), capturing the sequencing of events by the same thread in the execution's control-flow unfolding; reads-from (rf), relating a write event w with any read event r that reads from it; the coherence order (co), recording the execution's sequencing of same-address writes in memory; and read-modify-write (rmw), capturing which load/store exclusive instructions form a successful exclusive pair in the execution. The derived relation from-reads fr = rf -1 ;co relates a read r with a write w if r reads from a write w coherence before w. In addition, candidate executions also have relations capturing dependencies between events: address (addr), data (data), and control dependencies (ctrl). The relation loc relates any two read/write events that are to the same memory address.
We define the relation iseq, relating some write w to address x to an IC event completing a cache synchronisation sequence (not necessarily on a single thread): w is followed by a same-cache line DC event, which is in turn followed by a same-cache line IC event. In operational model terms, this captures traces that propagated w to memory, subsequently performed a same-cache-line DC, and then began an IC (and eagerly propagated the IC to all threads). In any state after this sequence it is guaranteed that w, or a coherence-newer sameaddress write, is in the instruction cache of all threads: performing the DC has cleared the abstract data cache of writes to x, and the subsequent IC has removed old instructions for location x from the instruction caches, so that any subsequent updates to the instruction caches have been with w, or co-newer writes.
Validation To gain confidence in the presented models we validated the models against the Arm architectural intent, against each other, and against real hardware. Validation against the Architecture To ensure our models correctly captured the architectural intent we engaged in detailed discussions with Arm, including the Arm chief architect. These involved inventing litmus tests (including, those described in §3 and many others) and discussing what the architecture should allow in each case. Validating against hardware To run instruction-fetch tests on hardware, we extended the litmus tool  [7]. The most significant extension consists in handling code that can be modified, and thus has to be restored between experiments. To that end, code copies are executed, those copies reside in mmap'd memory with (execute permission granted.
Copies are made from "master" copies, in effect C functions whose contents basically consist of gcc extended inline assembly. Of course, such code has to be position independent, and explicit code addresses in test initialisation sections (such as in 0:X1=l in the test of §3. 1) are specific to each copy. All the cache handling instructions used in our experiments are all allowed to execute at exception level 0 (user-mode), and therefore no additional privilege is needed to run the tests. To automatically generate families of interesting instruction-fetch tests, we extended the diy test generation tool  [3]  to support instruction-fetch readsfrom (irf) and instruction-fetch from-reads (ifr) edges, in both internal (samethread) and external (inter-thread) forms, and the cachesync edge. We used this to generate 1456 tests involving those edges together with po, rf, fr, addr, ctrl, ctrlisb, and dmb.
Making the models executable as a test oracle To make the operational model executable as a test oracle, capable of computing the set of all allowed executions of a litmus test, we must be able to exhaustively enumerate all possible traces. For the model as presented, doing this naively is infeasible: for each instruction it is theoretically possible to speculate any of the 2 64 addresses as potential next address, and the interleaving of the new fetch transitions with others leads to an additional combinatorial explosion. We address these with two new optimisations. First, we extend the fixed-point optimisation in RMEM (incrementally computing the set of possible branch targets)  [37]  to keep track not only of indirect branches but also the successors of every program location, and only allow speculating from this set of successors.
Using the Sail instruction semantics, we generate a Sail program that corresponds to each thread within a litmus test. The tool then partially evaluates these programs using the concrete values for addresses and registers specified in the litmus file, while allowing memory values and arbitrary addresses to remain symbolic. Using a Sail to SMT-LIB backend, these are translated into SMT definitions that include all possible behaviours of each thread as satisfiable solutions. The rules for the axiomatic model are then applied as assertions restricting the possible behaviours to just those allowed by the axiomatic model. The tool also derives the addr and data relations, using the syntactic dependencies within the instruction semantics to derive the syntactic dependencies between instructions.
Related Work To the best of our knowledge, no previous work establishes well-validated rigorous semantics for any systems aspects, of any current production architecture, in a realistic concurrent setting. The closest is Raad et al. 's work on non-volatile memory, which models the required cache maintenance for persistent storage in ARMv8-A  [39] , as an extension to the ARMv8-A axiomatic model, and for Intel x86  [38]  as an operational model, but neither are validated against hardware. In the sequential case, Myreen's JIT compiler verification  [33]  models x86 icache behaviour with an abstract cache that can be arbitrarily updated, cleared on a jmp. For address translation, the authoritative Arm-internal ASL model  [40, 41, 42] , and Sail model derived from it  [11]  cover this, and other features sufficient to boot an OS (Linux), as do the handwritten Sail models for RISC-V (Linux and FreeBSD) and MIPS/CHERI-MIPS (FreeBSD, CheriBSD), but without any cache effects.
Goel et al. [21, 20]  describe an ACL2 model for much of x86 that covers address translation; and the Forvis  [34]  and RISCV-PLV  [14]  Haskell RISC-V ISA models are also complete enough to boot Linux. Syeda and Klein  [49, 50]  provide an somewhat idealised model for ARMv7 address translation and TLB maintenance. Komodo  [16]  uses a handwritten model for a small part of ARMv7, as do Guanciale et al. [25, 12]. Romanescu et al. [44, 43]  do discuss address translation in the concurrent setting, but with respect to idealised models. Lustig et al. [30]  describe a concurrent model for address translation based on the Intel Sandy Bridge microarchitecture, combined with a synopsis of some of the relevant Linux code, but not an architectural semantics for machine-code programs.
Acknowledgements This work would not have been possible without generous technical assistance from  Arm. We thank  Richard Grisenthwaite ,  Will Deacon ,  Ian Caulfield , and  Dave Martin  for this. We also thank  Hans Boehm ,  Stephen Kell ,  Jaroslav Ševčík ,  Ben Titzer , and  Andrew Turner , for discussions of how instruction cache maintenance is used in practice, and  Alastair Reid  for comments on a draft. This work was partially supported by  EPSRC  grant  EP/K008528/1  (REMS),  ERC Advanced  Grant  789108  (ELVER), an  ARM iCASE award , and ARM donation funding. This work is part of the  CIFV  project sponsored by the  Defense Advanced Research Projects Agency (DARPA)  and the  Air Force Research Laboratory  (AFRL), under contract  FA8650-18-C-7809. The views, opinions, and/or findings contained in this paper are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the  Department of Defense  or the  U.