dataesr/scientific-paragraphs-categorization huggingface dataset:
In this paper, we present two recoverable software combining protocols, PBcomb which is blocking, and PWFcomb which is wait-free. We designed all five stages of our protocols taking into consideration three principles for reducing persistence cost (motivated by our experiments; also discussed in  [50, 54, 56, 4, 5] ), that are presented in Definition 2. Our experiments show that the resulting protocols are many times faster than a large collection of existing persistent techniques for achieving scalable synchronization. Definition 2 Persistence principles crucial for performance: 1. The number of the persistence instructions should be maintained as low as possible. This encompasses that an implementation must store in NVMM only those variables (and persist those values of them) that are necessary for recoverability.
Concurrent queues and stacks play a significant role in runtime systems  [1] , high performance computing  [30, 2] , kernel schedulers, network interfaces  [43] , etc. The proliferation of NVMM and the availability of highly-efficient recoverable stacks and queues could enable persistence in such settings. Based on PBcomb, we were able to design the first recoverable concurrent heap (PBheap); experiments show that PBheap has good performance when the heap is not too large. PBheap is useful for implementing recoverable versions of algorithms that rely on priority queues when the problem input size is small or medium. Implementations of concurrent heaps often do not scale well due to contention (mainly at the root node). This makes a heap implementation a natural candidate for applying software combining.
A thread p starts by recording its request, and (the reversed value of) its activate bit, in Request[p]. Next, it checks if the lock is acquired and if not, it tries to acquire it by executing a CAS. If it succeeds, p becomes the combiner and starts executing the combiner code (lines 14-28). Every thread q that does not become the combiner busy waits until the current combiner has released the lock. Then, q checks whether its request has been served; this is true when q's activate and deactivate bits are equal. If so, q returns its response value. The remaining threads contend again for the lock. In the combining code, a combiner p chooses among the two StateRec records of MemState the one, r , that is not indexed by MIndex , to use for serving requests. Then, in line 15, it copies the current state of the object into r.
Next, it executes a for loop (simulation phase), where for each thread q: If there is an active, valid request by q, p a) applies the request using r , ii) records the response into the appropriate element of the ReturnVal array stored in r , and iii) changes Deactivate[q] in r to make it equal to its activate bit. As soon as p completes the simulation phase, it changes MIndex to index r and unlocks Lock giving up its combining role. We say that req has taken effect at some point t, if a combiner p a) has read req in Request by t, b) has performed line 18 for q applying req, and c) has executed line 27 by t. We discuss the correctness of PBcomb in  [25]. To comply with persistence principle 1, PBcomb stores a number of its variables in DRAM. This results in improved performance. The algorithm can be easily modified to work correctly even if all data are stored in non-volatile memory.
PBHeap. PBheap is a persistent bounded min-heap implementation based on PBcomb. The state stored in StateRec is the array of heap elements and two integers identifying the bounds of the heap. PBheap supports the operations HGetMin, HInsert, and HDeleteMin. It employs a single instance of PBcomb and is implemented by enhancing a sequential heap implementation with the code of PBcomb. Memory Management. For ensuring persistence in allocating new stack or queue nodes, we follow a standard technique  [45, 17, 47]  where each thread p pre-allocates a fixed-size memory chunk in NVMM, and reserves nodes from this chunk. Whenever this chunk is exhausted a new memory chunk is allocated by p. If a garbage collection mechanism (for collecting nodes) is not used, whenever p serves as the combiner, it gets nodes in consecutive memory addresses (to comply with the persistence principles).
Performance Evaluation We evaluate our algorithms on a 48-core machine (96 logical cores) consisting of 2 Intel Xeon Platinum 8260M processors with 24 cores each. Each core executes two threads concurrently. Our machine is equipped with a 1TB Intel Optane DC persistent memory (DCPMM) and the system is configured in AppDirect mode. We use the 1. 9. 2 version of the Persistent Memory Development Kit  [44] , which provides the pwb and psync persistency instructions. An x86 64 store fence instruction is used for implementing a pfence operation. The operating system is Linux (kernel v3. 4) and we use gcc v9. 1. 0. Threads were bound in all experiments following a scheduling policy which distributes the running threads evenly across the machine's NUMA nodes  [22, 23]. For our experiments, we simulate an LL on an object O with a read, and an SC with a CAS on a timestamped version of O to avoid the ABA problem.
To avoid long runs and unrealistically low number of cache misses  [22, 21, 24, 40] , we added a local workload between consecutive executions of atomic operations, implemented as a short loop of a random number (maximum 512) of dummy iterations  [22, 21]. In Figure  1 , we compare the performance of AtomicFloat implementations based on PBcomb and PWFcomb against state-of-the-art wait-free persistent synchronization techniques: OneFile  [45] , CX-PUC  [18] , CX-PTM  [18] , and RedoOpt  [18] , using the latest version of code for these algorithms provided in  [16]. These algorithms satisfy durable linearizability (not detectable recoverability). Figure  1  shows that PBcomb is more than 4x faster than RedoOpt, which is the fastest among the competitors. Also, PWFcomb is more than 2. 8x faster than RedoOpt.
All these algorithms satisfy weaker consistency than detectable recoverability ensured by PBcomb and PWFcomb. Capsules  [10]  can be used to transform concurrent algorithms that use only read and CAS primitives to their persistent versions. The programmer has to partition the code into parts, called capsules, each containing a single CAS. This CAS has to be replaced with its recoverable version  [6]. We use an optimized version of Capsules, which can be applied only to normalized implementations  [51] , to our experiments, as it achieved better performance. Recent generic approaches for designing lock-free data structures appear in  [27, 29] ; they are not detectable recoverable and they do not experiment with stacks and queues. The first hand-tuned durable queues were provided in  [28]. One of them, namely the logqueue, ensured detectable recoverability, whereas the other two guaranteed durable linearizability  [35]  and buffered durable linearizability  [35] , respectively.
Discussion We present PBcomb and PWFcomb, highly-efficient recoverable software combining protocols that are many times faster than state-of-the-art recoverable universal constructions and software transactional systems. We identify three persistence principles, crucial for performance, and we illustrate how to make the appropriate design decisions to respect them when designing recoverable software combining protocols. Both PBcomb and PWFcomb can be used to derive recoverable implementations of any data structure from its sequential implementation. Thus, it is possible to develop a software-combining API that automatically transforms any data structure to fit our schemes by using a single instance of the corresponding algorithm. Our recoverable implementations of stacks, and the heap implementation, indeed follow this approach, using a single instance of PBcomb or PWFcomb.
To increase parallelism and achieve better performance, PWFqueue (and PBqueue) employs a similar approach as SimQueue  [21, 23]  utilizing two instances of PWFcomb (PBcomb, respectively). Although this choice is not fundamentally necessary and made the queue implementations more complicated than using a single instance, it results in superior performance. Coming up with a wait-free recoverable heap using PWFcomb is a relatively easy task. We are currently working on this direction, as well as on implementing a simple garbage collection scheme for PWFqueue. We will include the resulting algorithms in future versions of our library. Software combining restricts parallelism by executing sequentially all requests. Thus, PBcomb and PWFcomb, although applicable, are not necessarily the best choices for implementing e.
Detecting programming errors in software is increasingly important, and building tools that help developers with this task is a crucial area of investigation on which the industry depends. Leveraging on the observation that in Object-Oriented Programming (OOP) it is natural to define stateful objects where the safe use of methods depends on their internal state, we present Java Typestate Checker (JATYC), a tool that verifies Java source code with respect to typestates. A typestate defines the object's states, the methods that can be called in each state, and the states resulting from the calls. The tool statically verifies that when a Java program runs: sequences of method calls obey to object's protocols; objects' protocols are completed; null-pointer exceptions are not raised; subclasses' instances respect the protocol of their superclasses.
Checking for protocol subtyping is only the first step: as we will see in the next sections, we also need other mechanisms to correctly handle inheritance, method overriding and casting. In this paper, we present Java Typestate Checker (JATYC)  [18, 19] , a tool that type-checks Java source code where objects are associated with typestates. Java classes are annotated with typestates which specify the behavior of class instances in terms of available methods and state transitions. With JATYC, well-typed programs have the following properties: objects are used according to their protocols (typestates); protocols reach the end state (if the program terminates); null-pointer exceptions are not raised (in the code we can inspect). To ensure these properties, we follow the usual session type approach and force the linear use of objects associated with protocols.
JATYC is a new implementation of Mungo  [8]  that supports inheritance and adds critical features and fixes known issues, like assuming that a continue statement jumps to the beginning of the loop's body, thus skipping the condition expression  [19] , which may produce false negatives. It is freely distributed  6  and is implemented in Kotlin  [20]  as a plugin for the Checker Framework  [10] , which is actively maintained and well-integrated with the Java language and toolset. The major contributions with respect to the current version of Mungo are: -checking the absence of null pointer errors, which is critical to avoid the "The Billion Dollar Mistake"  [1] ; -checking that the protocols of objects are completed, i. e. protocols reach the end state, if the program terminates; -support for subtyping thanks to a synchronous subtyping algorithm, inspired in the work by Gay and Hole  [15] , Lange and Yoshida  [16] , and Bacchiani et al.
Protocol analysis and nullness checking To motivate the need for JATYC, consider a BaseIterator Java class that allows one to iterate over items of an array. List. 1 shows an implementation. 7 he intended protocol is defined implicitly by the sequences of method calls that are supported, and by the "states" reached via those calls. To use the BaseIterator, one must invoke the hasNext method before calling next, to ensure that there are remaining items to retrieve. If this contract is not followed, an IndexOutOfBoundsException will be thrown. While the Java compiler accepts code that does not follow this contract, in the next section we will show how to enrich Java classes with typestate annotations that allow rejecting programs containing these kinds of behavioral errors at compiletime. What JATYC allows one to do is to complement the code with protocol specifications and statically make sure these are respected and executed to completion (if the program terminates).
3). The. protocol extension is optional. Protocol compliance and completion. JATYC ensures that instances of Java classes associated with a typestate obey to the corresponding protocol and reach the end state, so that potentially important method calls are not forgotten and resources are freed. To see an example of incorrect use of BaseIterator, consider List. 4, where errors are indicated in the comments. According to the protocol (List. 2), we can only call next if the hasNext call returns true, but the code is doing the opposite (notice the negated condition in line 2). This results in an error stating that we cannot call next in state end and that the protocol was not completed. Removing the negation fixes both issues. Nullness checking. Null pointer errors are the cause of most runtime exceptions in Java programs  [4, 21] : being able to detect these errors at compile-time is therefore crucial.
Method inheritance Inheritance makes it possible to reuse methods from superclasses, override some, or add new ones. For example, the code presented in List. 7 shows an example of safe class inheritance: the RemovableIterator class implements the protocol presented in List. 2 and extends the BaseIterator class. In particular, the RemovableIterator class, differently from the BaseIterator, uses a Java List as the underlying data structure and consequently all the methods need to be overridden in order to access the collection. Moreover, according to its protocol, the class presented in List. 7 implements the new remove method. To correctly support inheritance, we consider the following cases: 1. A class without protocol extending a class without protocol. The first and second scenarios are trivially handled: the former does not require any inspection since classes by default do not have protocols; and the latter is checked using the subtyping algorithm.
Acknowledgements This work was partially supported by the  EU   H2020 RISE programme  under the  Marie Skłodowska-Curie  grant agreement No. 778233  ( BehAPI ) and by  NOVA LINCS  ( UIDB/04516/2020  and  UIDB/04516/2020/TRA/BIM/07 ) via the Portuguese Fundacão para a Ciência e a Tecnologia.
metadata description Current software version 3. 0 Permanent link to executables of this version https://github. com/jdmota/java-typestate-checker/releases/tag/3. 0 Permanent link to Reproducible Capsule https://codeocean. com/capsule/5619420://github. com/jdmota/java-typestate-checker/wiki/Documentation Support email for questions jd. link to code/repository used for this code version https://github. com/ScienceofComputerProgramming/SCICO-D-21-00203 Permanent link to Reproducible Capsule https://codeocean. com/capsule/5619420://github. com/jdmota/java-typestate-checker/wiki/Documentation Support email for questions jd.
I. INTRODUCTION Cloud infrastructures enable the building of elaborated services through the composition and configuration of multiple computing resources, such as virtual machines, network devices, and software components. These elementary resources may typically be deployed across different infrastructures supported by one or several cloud provider(s), and are subject to changes over time  [1]. This dynamics increases the complexity of management tasks and may lead to potential vulnerabilities that may compromise the resources, or even the whole cloud composite service. In particular, the cold and hot migrations of cloud resources are currently facilitated by Supported by the project CONCORDIA that has received funding from the European Union's Horizon 2020 research and innovation programme under grant agreement No.
B. Security framework for cloud migration In order to address these automation challenges, we have designed a security framework for supporting resource migrations in cloud composite services. The different building blocks of this framework and their interactions are illustrated on Figure  2. The framework is triggered when a resource of the composite service undergoes a migration. This composite service, represented on the top of the figure, is orchestrated using the TOSCA orchestration language, which describes its elementary resources as well as their relationships. Concretely speaking, the TOSCA language specifies a cloud service as a TOSCA topology which defines a set of TOSCA nodes (e. g. a web micro-service node) that are interconnected by a set of TOSCA relationships (e. g. the interconnection to a MySQL database node).
Orchestrated Cloud Composite Service Fig. 2 : Main building blocks of the considered security framework for cloud migration tions using the Open Vulnerability and Assessment Language (OVAL)  [22] , and security function descriptions that reuse the same specification to define the counter-measures that can be applied on the cloud resource in an endogenous or exogenous manner. The OVAL language, part of the Security Content Automation Protocol (SCAP)  [23]  developed by NIST, has become the de-facto standard for describing configuration vulnerabilities in a machine readable manner. Common Vulnerabilities and Exposures (CVE) definitions that only provide literal descriptions, it specifies each vulnerability as a logical combination of tests/conditions that if observed on the target system, the security problem described by such vulnerability is present on that system.
• migrate : C × M → S ≡ function that corresponds to a migration m ∈ M applied on a component c ∈ C, and that returns the state of the component c after the operation of the given migration. The assessment of the migrated resource is performed based on a set of vulnerability descriptions V = {v 1 , v 2 ,. , v m }. For instance, one of these descriptions refers to the CVE-2017-5638 presented in the illustrative example. As each vulnerability description can be specified as a logical formula corresponding to a state s ∈ S, the vulnerability dataset can be seen as a disjunction of logical formulas given by φ = v 1 ∨ v 2. ∨ v n = (v i ) with v i ∈ V. Considering these definitions, we specify an assessment function Φ : S → Boolean that determines if a component c ∈ C is vulnerable under V , meaning that the assessment of φ over the state of c is true.
We then exploit the assessment function Φ to support the selection of counter-measures using Equation  2 , where Π(impact(m i ), state(c)) provides the resource projection after migration, and the Π function is used a second time on this projection to assess the resource state after the application of the security functions using f uture(F ). Φ(Π(f uture(F ), Π(impact(m i ), state(c)))) m i ∈ M, F ⊂ F, c ∈ C (2) Once the security functions are properly selected by the security framework, their application can be effectively performed using the activate(F , c) function over the cloud composite service, in a proactive or reactive manner. We have then evaluated the performance of the proposed security framework through extensive series of experiments. In that context, we have developed a proof-of-concept prototype written in Python, which supports the different blocks of the framework, and is built on top of the open-source CVC4 SMT solver.
The prototype internally generates a SMT-LIB (Satisfiability Modulo Theories LIBrary) specification, which can also be interpreted by other SMT solvers, such as Z3 and VeriT. We have performed the experiments over a regular laptop equipped with a 2Ghz Intel Core i5 processor and 8GB of RAM memory. We have considered a simple TOSCA specification, and have used vulnerability descriptions coming from the official OVAL repository, considering the specifications for various operating systems corresponding to the largest datasets, namely CentOS Linux, RedHat Enterprise Linux and Microsoft Windows with different versions. The same OVAL formalism is exploited for defining the tests that are used to characterize the configuration states and their properties, and for specifying the description of security functions that are applicable for the cloud resource, such as the application of patches or the activation of a web application firewall with specific security rules.
A. Distribution of vulnerability properties In a first preliminary series of experiments, we were interested in assessing the distribution of properties (or tests) amongst the considered vulnerability descriptions, each OVAL test being associated to a given property. The objective was to quantify the redundancy of tests that are used to evaluate properties for the vulnerability datasets. For that, we have analyzed the OVAL datasets for the different operating systems, and measured the occurrence of tests for each of them. We considered five different occurrence categories using a logarithmic scale, with tests that are present respectively once, up to 10, up to 100, up to 1000, and up to 10000 times in a vulnerability dataset. We have observed that a large proportion of tests (or properties) are present between 2 and 10 times, representing on average 44,15% for the different datasets.
The other highest categories are less significant with around 8,22% of tests that occur between 11 and 100 times, and less than 1% on average for tests occurring up to 1000 and 10000 times. The distributions are relatively homogeneous amongst operating systems, with the highest values of occurrences being observed with the Microsoft Windows operating system. This distribution analysis shows that more than half of the tests or properties (around 53% on average) occur more than once in the different datasets, arguing in favor of our solution based on SMT solving, which is usually efficient in simplifying such satisfiability problems with redundant constraints.
B. Performance of migrated resource assessment In next series of experiments, we wanted to quantify the time required for translating the vulnerability descriptions into logical specifications, and for assessing the projection of the cloud migrated resource with respect to the different vulnerability datasets. Figure  5  describes the time required by the security framework to automatically translate a vulnerability dataset V into a logical specification with a conjunctive normal form that is then directly interpretable by the SMT solver. Our framework generates a conjunctive normal form by construct, in order to prevent any additional pre-processing to be performed by the solver afterwards. The figure details the translation time for each operating system dataset, with regard to the number of vulnerabilities and properties.
We can In the meantime, Figure  6  depicts the evaluation time required for assessing the projection of the migrated resource with respect to a given vulnerability dataset. The time includes the interpretation of the SMT-LIB specification together with the solving of the satisfiability issue. We can observe a linear behavior with respect to the number of tests (or properties). The minimal evaluation time has been obtained with RedHat Entreprise Linux 5, corresponding to the smallest dataset, while the maximal time corresponds again to Microsoft Windows 2012R2, which is the largest dataset. The evaluation time is clearly smaller than the translation time, and is kept under 1,6 seconds for all the vulnerability datasets, confirming the feasibility of our approach. The translation activity should rather be performed proactively, as soon as the publication of new vulnerability descriptions.