Cyclic proof systems are sequent-calculus style proof systems that allow circular structures representing induction, and they are considered suitable for automated inductive reasoning. However, Kimura et al. have shown that the cyclic proof system for the symbolic heap separation logic does not satisfy the cut-elimination property, one of the most fundamental properties of proof systems. This paper proves that the cyclic proof system for the bunched logic with only nullary inductive predicates does not satisfy the cut-elimination property. It is hard to adapt the existing proof technique chasing contradictory paths in cyclic proofs since the bunched logic contains the structural rules. This paper proposes a new proof technique called proof unrolling. This technique can be adapted to the symbolic heap separation logic, and it shows that the cut-elimination fails even if we restrict the inductive predicates to nullary ones.

At present, to deal with a large amount of variety data in the database, various NoSQL databases have been proposed and put to practical use. However, since most of them support the transaction processing only on the single data, there is the problem that the plural data cannot be updated in a lump with maintaining the ACID properties. To solve this problem, in this paper, we propose a method to process plural data as a single transaction for MongoDB, which is a kind of document oriented NoSQL database. Concretely, each data has both of the before and after update fields, and the state of the transaction is managed. Then, in the case of before the commit, the former data is queried; after the commit, the latter data is queried. By this method, we show that the plural data can be updated as a transaction with the specified isolation level.

Databases of business systems are generally updated by two methods: the online entries reflect the input from a lot of terminals immediately; the batch update updates a great deal of data in a lump. Here, the batch update usually takes time. So, in the case where it is performed as a single transaction by using the lock, the conflicting online entries wait for a long while. For this problem, we had proposed the temporal update method, and showed the both can be executed concurrently by it. However, to process them by a serializable schedule, the execution timing of the online entries has to be divided by the batch update. So, it raises a problem that there are still latencies of some online entries by this. In this article, we propose four concurrency control methods to shorten this wait. And, we show their implementations and evaluation results. Moreover, we show the appropriate method should be chosen based on the operational requirements

Abstract Today, distributed business systems are used widely, and the consistency of their databases are maintained by the distributed transactions. On the other hand, a great deal of data is often updated in a lump-sum in the business systems. And, since the non-stop service has become general, it is necessary to perform this lump-sum update concurrently with the online transactions that service to users. So, some methods are utilized to avoid the influences on the online transactions, like the mini-batch that splits a lump-sum update into small transactions and executes them one after another. However, in the distributed systems, since it has to be executed by the distributed transactions, there is a problem on the efficiency to update a great deal of data by this method. For this problem, we propose to apply an update method to the distributed systems, which utilizes the records of data about the time to avoid conflicts between the lump-sum update and the online transactions. Moreover, through experiments using a prototype, we confirmed that it can update data more efficiently than the chain of small transactions even in the distributed systems.

In business systems, databases are usually updated by two methods: the online entry is used for update from many terminals concurrently; the batch update is used to update a great deal of data in a lump. Since online entry updates a small amount of data, concurrency control can be performed by locking the data. On the other hand, the batch update locks a great deal of data for a long while. So, if it’s performed concurrently with online entry, it’s performed as the mini-batch that divides the update to shorten the lock time of each unit. However, because this method cannot treat the entire batch update as a single transaction, various constraints occur on system operations. In this paper, we propose a batch update method utilizing the transaction time database that manages the history of time series of its data. And, we show that the ACID property of the transaction can be maintained by this method as a whole batch update.