Search

Modern processors deploy a variety of weak memory models for efficiency reasons. Total Store Order (TSO) is a widely used weak memory model which omits store-load constraint by allowing each core to employ a write buffer. Partial Store Order (PSO) is similar to TSO, but in consideration of higher performance, it does not guarantee that writes to different locations propagate to the shared memory following the program order. For understanding the reordering appearing in PSO precisely, we analyze this memory model by utilizing formal methods. In this paper, we apply Communicating Sequential Processes (CSP) to model PSO. By feeding the constructed model into the model checker Process Analysis Toolkit (PAT), we verify four properties. The requirements of TSO are more stringent than PSO, and then PSO must preserve write-read reordering and read-after-write elimination defined by TSO. The programs containing store-store fences between every two writes have the same outcomes under TSO and PSO, which is called outcomes consistency. Last but not the least, PSO should satisfy write-write reordering which indicates that two writes by the same thread may be reordered if they target different locations. [ABSTRACT FROM AUTHOR]

Fertilizer-induced CO2 emission is a primary driver of global warming. The experiment was used to study whether controlled-release urea (CRU) application in winter oilseed rape can play a positive role in mitigating CO2 emission and promoting C utilization by soil microorganisms. Five fertilizer types consisted of N0 (0 g N plant−1), conventional CRU application (CRU100%), monotypic CRU at the 80% of conventional rate (CRU80%), co-application of CRU with uncoated urea (CRC), and organic fertilizer (CRO). Results showed that soil CO2 fluxes were significantly affected by N fertilizer types after the start of the stem growing (P < 0.05). CO2 emissions typically peaked during the seed filling period, with the highest emission of 1.99 μmol m−2 s−1 being registered for CRU100%. CRU100% had 25.00%, 30.60%, and 4.17% greater CO2 emissions than CRU80%, CRC, and CRO practices by harvest, respectively. Compared to the conventional CRU treatment, CRU80% led to a lower root volume and root mass ratio than CRU100%, which could partly contribute to the reduced CO2 emission. Conversely, CRU80% performed better in N agronomic efficiency than that of CRU100% treatment. Also, C source utilization by soil microbiomes as well as microbial diversity indices following CRU80% along with CRO applications was substantially higher than that under the conventional CRU supply. These observations suggest that opportunity exists to maintain N balance by N fertilization practices to mitigate CO2 emission from cropland. Further, a close and positive relationship between soil total nitrogen and CO2 emission also supports this. CRO-treated soils substantially elevated the contents of total carbon and readily oxidation carbon over CK. Moreover, the enzyme activity of β-glucosidase in CRO soil was about twice as high as the CRU100%. Consequently, CRU amendments by decreasing CRU rate application and the incorporation of organic fertilizer into CRU have the potential for mitigating of CO2 emission and positive effect on the soil microbial functional diversity to improve nitrogen use efficiency of rapeseed. [ABSTRACT FROM AUTHOR]

Metaheuristic algorithms (MHs) have a long history that can be traced back to genetic algorithms and evolutionary computing in the 1950s. Since February 2008, with the birth of the Firefly algorithm, MHs started to receive attention from researchers around the globe. Variants and new species of MH algorithms have bloomed like sprouts after rain. However, the necessity for creating more new species of such algorithms is questionable. It can be observed that these algorithms are fundamentally made up of several widely used core components. By explaining these components, the underlying design for a collection of the so-called modern MH optimisation algorithms is revealed. In this paper, the core components in some of the more popular MH algorithms are reviewed, thereby debunking the myths of their novelty, and perhaps dampening claims that something really 'new' is invented simply by branding an MH search method with the name of another living creature. Counterintuitive experimentations have shown that by taking snapshots, anyone can show some improvements of an MH over another in some situation. Mixing certain components up indeed adds advantage over the original MH. The same goes to extending MH with slight functional modification. This work also serves as a general guideline and a reference for any algorithm architect who wants to create a new MH algorithm in the future. [ABSTRACT FROM AUTHOR]

Abstract. An action system is a framework for describing parallel or distributed systems, for which the refinement calculus offers a formalisation of the stepwise development method. Fairness is an important notion in modelling parallel or distributed systems, and this paper investigates a calculus for refinement of lair action systems. Simulations, which are proof techniques for refinement, are extended to verify fair action systems. Our work differs from others' in that the additional condition concerning fairness is expressed through termination of related iteration statements. For this purpose, existing proof rules for termination are extended. In the tradition of the refinement calculus, our approach to fairness is based on techniques developed mainly for sequential programming. [ABSTRACT FROM AUTHOR]