--
You received this message because you are subscribed to the Google Groups "Hafnium" group.
To unsubscribe from this group and stop receiving emails from it, send an email to hafnium-discu...@googlegroups.com.
To post to this group, send email to hafnium...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/hafnium-discuss/44fb8c73-4b49-461a-af7c-ea83381b52e8%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
To view this discussion on the web, visit https://groups.google.com/d/msgid/hafnium-discuss/CA%2B_y_2Gcgg%3D%3DpOBJkct%2BumomL-69Cxs5F4Sszhck9u8bHss_Jw%40mail.gmail.com.
I'm going to take a closer look at the changes but I'm interested as to why you suggest finer grained locking will make arguments of correctness easier?
I submitted Gerrit review request. I'm new to Gerrit, and it's totally different from GitHub... Please correct me if I'm doing anything wrong. Please review the following diffs:Preparing the review request, I realized that I don't need to split the vcpu lock into two. Interrupt information is accessed only by the running, current vcpu, which already has the lock in the new scheme. In short, (1) the vcpu's lock protects its state, register file, and interrupt information; and (2) the running pcpu conceptually has the running vcpu's lock. It's review id 5460.
Now I realized that `VCPU_STATE_RUNNING` is no longer needed. A running vcpu's lock is already acquired, so it's state cannot be read by any threads. So I removed it. It's review id 5461.Thanks,Jeehoon
On Saturday, June 1, 2019 at 7:49:21 PM UTC+9, Jeehoon Kang wrote:Thank you for feedback!I'm going to take a closer look at the changes but I'm interested as to why you suggest finer grained locking will make arguments of correctness easier?My general strategy here is associating data, not code region, to a lock. Because using locks we want to remove concurrent accesses to a shared data, not code region. This strategy is shared among concurrent programming literature, and is culminated by the following interface of mutex in Rust: https://doc.rust-lang.org/std/sync/struct.Mutex.html#method.lock Of course we can do a similar thing in C++.Back to Hafnium, I think the current locking scheme in vcpu doesn't clearly state which data is protected by which locks. My branch tries to clarify the relation: the "execution lock" protects state and the register file, and "interrupts lock" protects interrupt things. The reason why a running vcpu is locking the execution lock is, it is changing its state and register file. This should increase the number of locks---as we want to inject interrupts to a running vcpu---but it better reflects our intention and is easier to verify than using a single lock, IMO.
--
You received this message because you are subscribed to the Google Groups "Hafnium" group.
To unsubscribe from this group and stop receiving emails from it, send an email to hafnium-discu...@googlegroups.com.
To post to this group, send email to hafnium...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/hafnium-discuss/f2d8ca15-9aa6-450d-853d-57027b11eac3%40googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/hafnium-discuss/CA%2B_y_2HxXr%2B8drOh3vt%2BuGDWHGqQWwpSoeMndywCTyYvZKAyRg%40mail.gmail.com.