SOSP 2009: Day 2

I/O

Better I/O Through Byte-Addressable, Persistent Memory

  • DRAM is fast, byte-addressable and volatile, but disk/Flash are non-volatile, but slow and not byte-addressable. BPRAM is all three!
  • Phase change memory is a promising source for this. Bits encoded as resistivity. Access latency in the nanoseconds, and far better endurance than flash. Designed BPFS for BPRAM.
  • Goal: FS ops commit atomically and in program order. Data is durable as soon as the cache flushes. Use short-circuit shadow paging to get this (new consistency model).
  • Eliminate DRAM buffer cache; use L1/2 instead. Put BPRAM on the memory bus. Provide atomicity and ordering in hardware.
  • Both BPRAM and DRAM are addressable by the CPU: physical address space is partitioned into volatile/non-volatile.
  • BPFS gets better performance than NTFS on the same media.
  • What happens on crash during update? Short-circuit shadow paging comes into play (contrast with journalling or shadow paging). Overhead of journalling is that all data (or metadata) must be written twice. Shadow paging uses copy-on-write up to the root of the FS: drawback is that writes propagate all the way back to the root (multiple updates), and small writes have a large copying overhead.
  • Short-circuit shadow paging makes in-place updates where possible. Uses byte-addressability and atomic, 64-bit writes. Both in-place updates and appends are made simple by this technique. Cross-directory rename does bubble up to the common ancestor.
  • Problem: if data is cached in L1/L2, the ordering of cache eviction can lead to inconsistent states. Also, writes from the cache controller might not be atomic.
  • So add two new hardware components to the CPU and cache controller. Epoch barriers are used to declare ordering constraints and they are much faster than a write-through cache. Also add capacitors to DIMMs which allow writes to propagate even after the loss of power.
  • Do CoW then Barrier then Commit. Paper also shows how to make it work on multiprocessors.
  • Built and evaluated on Windows as an in-kernel file system.
  • Microbenchmarks (append n bytes and random n-byte write) compare NTFS/Disk, NTFS/RAM and BPFS/RAM. (Using DRAM in this experiments.) BPFS is significantly faster than NTFS on disk, and NTFS isn’t syncing so it isn’t durable!
  • Postmark benchmark compares NTFS/Disk, NTFS/RAM, BPFS/RAM and (projected) BPFS/PCM. BPFS/PCM is much faster than both NTFS/Disk and NTFS/RAM. Analytical projection based on sustained throughput of PCM.
  • Q: are the storage requirements of a database and of a file system converging when you have this hardware available? The changes to the hardware will be applicable to other sorts of storage systems like a database, not just filesystems.
  • Q: have you thought about how to expose more capabilities of this medium to the applications (not just sequential reads and writes)? Applications are currently written in terms of what is efficient.
  • Q: how do you atomically deal with a free-list? We don’t have a free-list. Don’t need to keep track of so many data structures because the medium is so fast, which lowers the consistency overhead.
  • Q: where do you go next for multiprocessors and clusters? One of the goals was to have multiple concurrent threads operating on the FS at the same time.
  • Q: is there a risk that data in the capacitor gets garbled after the machine gets switched off? [Taken offline.]
  • Q: could you go even faster without having the consistency guarantees, for applications that don’t need it? There’s always a trade-off here.
  • Q: how do you do mmap, and is meddling with L1/L2 caches going to be expensive? Haven’t implemented mmap yet, but we would have a much better guarantee of durability. Changes to the cache, in the paper have been looked at in terms of interference, and performed well.
  • Q: why didn’t you benchmark against a file system using a B-tree or a red-black tree that can take advantage of random writes [why did you compare against NTFS]? NTFS is widely used, and it’d be interesting to compare against others.

Modular Data Storage with Anvil

  • Data storage drives modern applications (everyone has a database) and they are frequently a bottleneck. Hand-built stores outperform general-purpose ones by up to 100x. Observe that changing the layout can substantially improve performance. Custom storage is hard to write, especially in order to provide consistency guarantees. Can be prohibitively expensive to experiment with new layouts.
  • Need a simple and efficient modular framework to support a wide variety of layouts.
  • Fine-grained modules: dTables. These are composable to build complex data stores. All writing is isolated to dedicated writable dTables, which incidentally has good disk access properties.
  • dTable = key/value store. Maps integers/floats/strings/blobs to blobs. Provides an iterator to support in-order traversal. dTables used by applications and frontends, and also other dTables. Can transform data, add indices or otherwise construct complex functionality from simple pieces.
  • Example of a mapping from customer IDs (mostly contiguous) to states. Start with an array dTable for the common case. Layer a dictionary on top of that (maps state names to array indices). Have an exception dTable for the case where a customer isn’t in one of the 50 states, and a linear-search dTable for their residences. But to make this fast, layer a B-Tree index dTable on top of the linear store.
  • So far just read-only. Updates are hard to do transactionally. Need to implement a write-optimized dTable. Fundamental writable dTable is the journal dTable. New data is appended to a shared journal; data are cached in an in-ram AVL tree. The journal is digested when it gets large. Transaction system is described in the paper. Layer this over read-only dTables.
  • Managed dTable goes at the top. Also have a Bloom filter dTable to deal with multiple overlaid read-only dTables.
  • Many additional dTables listed in the paper.
  • Evaluate  the effect of simple configuration changes on performance (modularity). Key lookup workload, comparing contiguous versus sparse keys. Contiguous good with arrays; sparse good with B-trees. Also show the benefit of layering an index on top of a linear store. Also show the low overhead of the Exception dTable.
  • Evaluated by running TPC-C. Replaces a SQLite backend with Anvil. Shows that Anvil outperforms both the original backend and MySQL. Split read and write stores perform well.
  • Evaluated the cost of digesting and combining. These can be done in the background, taking advantage of additional cores and spare I/O bandwidth. Measured the overhead when doing a bulk load (1GB) into the dTable, with digests every few seconds.
  • Q:  why didn’t you compare either performance or features against BDB, which is very similar? Didn’t find it as easy to construct read-only data stores in BDB: creating customisable data stores has a lot of transactional overhead.
  • Q: did you evaluate iteration? In paper. How does the performance depend on the order of updates? Not sure what you mean. Did look at overlay iteration in the paper, which ought to be the most expensive (due to key lookup cost), and overhead was only 10%
  • Q: how did you make it so that the creator of a new dTable doesn’t have to consider ACID semantics? Most dTables are read-only, so you don’t need to worry about this (like shadow paging). The managed dTable has a small hook that enforces transactional semantics. And read/write dTables? Don’t envision that people will need to create these. Could implement your own, but this would miss the point.
  • Q: how should developers write recovery tools for systems like Anvil? Anvil includes such a tool that handles recovery for you. Read-only semantics makes this much simpler.

Operating Systems Transactions

  • [Unfortunately, I missed this talk due to having an obligation to man the registration desk. I'll try and track down the video and update this later.]

Parallel Debugging

Do You Have to Reproduce the Bug at the First Replay Attempt? — PRES: Probabilistic Replay with Execution Sketching on Multiprocessors

  • Concurrent programs are hard to write. Multi-core makes concurrent programming more important, and bugs more common. However they are non-deterministic (requiring e.g. a special or improbable thread interleaving). This makes it hard to reproduce them.
  • Deterministic replay for uniprocessors is relatively easy: only need to record inputs, thread scheduling and return values of system calls. On multiprocessors, this is much more challenging. e.g. Simultaneous memory accesses are another source of non-determinism.
  • Previous proposals introduce new hardware, which don’t exist in reality. Or there are software-only approaches but they have up to 100x slow-down.
  • Ideally want to reproduce a bug with a single replay and no runtime overhead. But what if we relax this slightly?
  • Idea 1: record only partial information during a production run. Idea 2: push the complexity into diagnosis time. Idea 3: use feedback from unsuccessful (non-reproducing) replay runs.
  • Just record a sketch during the production run. When a replay goes off the sketch, terminate it immediately and feed back information about why it deviated for refining the next replay. Can eventually reproduce the bug with 100% probability.
  • Several different methods for sketch recording. Spectrum of approaches from UP deterministic replay to full MP DR. Can record e.g. synchronization points, or basic blocks, or more: build up this information during the replay runs.
  • At replay time, the partial information replayer consults the sketch to see that recorded global ordering is obeyed. How do we know whether a replay is successful? Use a failure detector based on crash, deadlock or incorrect results. This can also detect unsuccessful replay runs.
  • When a replay attempt fails, start it again. But could do something different the next time: a random approach would just leave it to fate, but PRES is more systematic. Failed reproduction is due to un-recorded data races. The feedback generator captures these races and tweaks them in future runs. Start with many candidate races and filter them down.
  • Implemented PRES using Pin. Evaluated many different applications (desktop, server and scientific). Overhead is around 18%, which is barely more than baseline Pin overhead. Macrobenchmarks show that PRES gets much higher throughput for server applications (MySQL).
  • Effectiveness: UP algorithm doesn’t detect any bugs within 1000 replays, whereas PRES gets 12/13 in 10 attempts. Feedback generation is crucial to effectiveness. Race filtering also effective.
  • Q: could you also use execution traces to help track down which parts of the execution trace cause the bug to not happen, and guide the programmer? Good idea.
  • Q: could you apply PRES to virtual machine replay? Also a good point. The work could be integrated with virtual machines. Could you rollback an execution, is it precise enough? Depends on the fine-grainedness of the recording scheme used. What is the inherent overhead in collecting a trace with sufficient fidelity to do backtracking? If there is a lot of lock operations, the low-overhead approach (SYNC) could work. But if there is no synchronization, we can’t use this information, and a more heavyweight scheme would be needed.
  • Q: why do the results differ so much from the next paper? The main idea is similar, but their work is more focussed on static analysis to reduce runtime overhead.
  • Q: would you advocate this as a solution for long-running (one year or more) services, as it is often only after this time that they emerge? We can take a checkpoint of the process state, which solves the problem of data accumulation. 

ODR: Output-Deterministic Replay for Multicore Debugging

  • Debugging non-deterministic software failures is really hard. The problem is how to reproduce these failures for debugging. Model checking/testing/verification could work, but it’s not perfect, and it doesn’t capture everything. So we need deterministic replay.
  • Need multiprocess operation, efficient recording, no special hardware and the ability to run arbitrary programs without annotation (especially programs with data races). All related work fails to meet one of these requirements.
  • ODR is a user-level replay system, which works in the MP case, has only 1.6x overhead, needs no new hardware and works on arbitrary x86 Linux binaries.
  • Often sufficient to produce any run with the same outputs… needn’t have the exact same execution. So the idea is to relax the determinism requirements.
  • The classic guarantee is value determinism: replay run reads and writes must have the same values as the original. Relax this to “output determinism”: the replay run produces the same user-visible output as the original. This is not perfect, but still useful for debugging: reproduces most visible signs of failure, and enables reasoning about failure’s root cause.
  • How to achieve this? Deterministic-run inference. Basic idea is to translate a program into a logical formula (verification condition). Function of schedule trace, input trace and read trace, returning an output trace. Use a formula solver to yield unknown schedule trace. Scale this by directing the inference using more original-run information. Also by relaxing memory consistency of the inferred run: where values read have nothing to do with schedule order, can use an arbitrary schedule trace.
  • Three-dimensional inference design space: memory consistency (strict, lock order or null), query complexity (output, I/O&lock-order, I/O&lock-order&path or determinant), and inference-time (polynomial or exponential). Search- and query-intensive DRI fit into this space.
  • Search-intensive is really slow (400–60000x slowdown). Formula generation, not solving is the bottleneck. Use multi-path symbolic execution with backtracking to generate formulas. Each backtrack involves a 200x slowdown. Backtracks are caused by race-tainted branches: wrong choice leads to a divergent, unsatisfying path. Work around by backtracking to the most recent race-tainted branch.
  • If we know the path (QI-DRI), inference time improves by 100x but we need to record much more data, so there is a 6x slowdown.
  • Future work is to reduce the path-search space, reduce the cost of each backtrack (cut down on race-tainted branch analysis), and parallelize formula generation by forking threads at each divergence.
  • Q: if I put in arbitrary values in the memory consistency model, how do I ensure that invariants are maintained? We don’t actually do null consistency, but if we did and invariants were violated the program might crash and output determinism catches this (because the output would be different).
  • Q: since your techniques are similar to the last paper, why are the results so different? In our approach, we do race-tainted branch analysis for the entire exectuion, and that is costly. We also do taint-flow propagation. There is more analysis in each backtracking iteration than theirs. We could reduce this cost by, for example, reusing results from previous iterations.
  • Q: have you considered changing your static analysis to another algorithm that could significantly improve your formula generation time? We are considering static approaches to formula generation.

Works-in-Progress

  • RAMCloud: Scalable, High-Performance Storage Entirely in DRAM. New research project. Zero results. Motivated by wanting to build large scale systems with low latency. Data center style of web application separates the code from the data, in order to scale, but 4–5 orders of magnitude increase in latency. Want this kind of scaling with latency close to memory speeds (sub-microsecond). Basic architecture puts all data in DRAM. Scale using commodity servers. Reckon we can get 5–10us RPC latency end-to-end. Also have a story on durability and availability. Also want to support multiple applications.

    Q: effect of other memories? Whichever wins should work with RAMCloud

    Q: GMS system from UW 10 years ago? Not familiar with that [taken offline].
  • Transactional Caching of Application Data using Recent Snapshots. DB-driven website performance issues: use memcached. Add an in-memory DHT that is very lightweight, and stores application objects (not a DB). DBs provide transactional consistency, but these caches don’t do this. Goal is transactional consistency for accesses to the cache. Idea is to embrace staleness: all read-only transactions to run on stale data. Avoids blocking and improves utilization. This is quite safe, since stale data is already everywhere. Application can control staleness. Add a TxCache library between memcached and the application. DHT values are timestamped, and have a validity interval.

    Q: paper at HotStorage from HP Labs in similar area?

    Q: how does the DB know the validity interval? Modified DB to track this.
  • Chameleon: A self-managing, low cost file system. Targeting home user or small business, who doesn’t want to lose data. Doesn’t know anything about RAID. Cost-sensitive. Deployment scenario has 4 PCs connected by fast LAN, with a broadband connection to cloud storage. There are many ways to replicate, place and encode data. Ideally store data on at least one offline device to avoid vulnerability to viruses. A small, trusted “anti-availability kernel” enforces this requirement. Use linear programming to select and adapt storage configuration: the design space is now even more complicated. Tend towards the optimal solution.
  • Sloth: Let the Hardware Do the Work!Looked at embedded OSes used in the automotive industry. OSEK OS is the prevalent real-time embedded OS: event-triggered, priority-driven real-time system. Don’t want to implement a scheduler. SLOTH lets the interrupt subsystem do the scheduling and dispatching work. All threads are implemented as interrupt handlers and have interrupt priorities. Each thread needs an IRQ source. Priorities enable pre-emption. Can implement a bunch of synchronization this way also. System is simple, small (concise implementation and memory footprint) and fast (2–20x).

    Q: this looks like very simple scheduling… how would you deal with something more complicated like earliest deadline? Drawback is no blocking system calls, so can’t do everything.
  • The case for cooperative kernel threads. Kernels are multithreaded, and drivers have concurrency bugs, which, if they are in the kernel, is bad. Event-based devices drivers need to use continuations to preserve driver context across blocking operations. This becomes very complex, almost as bad as dealing with pre-emptive threads. Cooperative threads give the best of both worlds: atomic execution but allowing blocking. Research showed that drivers are mostly I/O bound, so cooperative threads are appropriate. Implementing this as a “cooperative domain” in the Linux kernel.

    Q: Linux does have cooperative thread scheduling available, so how does this interact with the work you are doing? Providing a framework for implementing drivers this way, much nicer.
  • Abstractions for Scalable Operating Systems on Manycore Architectures. Tesselation. Goal isn’t just to support heterogeneous hardware, but also provide predictable performance and guarantees for applications. Asymmetrically structured OS: some cores are dedicated as a management unit for keeping track of and scheduling applications. Eliminates the need for per-core runqueues, improves cache locality, decreases lock contention and limits kernel interference with applications. Applications interact with the kernel through remote, asynchronous system calls. Applications make explicit requests for cores, and OS guarantees that they will be gang-scheduled. OS just provides cores to the application, doesn’t need to know about threads. Applications have private memory ranges.

    Q: how do you balance the different demands for resources across applications? [Taken offline.]
  • System Support for Custom Speculation Policies. Applications run on some speculation infrastructure, which speeds things up. Want to separate policy from mechanism. Typically implemented transparently, which means that you have to be conservative, giving limited opportunities for speculation. Idea is to push the policy into the application. What could an application do that is different from the default? Might allow some output to be uncommitted. Or could commit equivalent-but-not-identical results. Process gets a “speculative fork” interface. Use cases: predicting user actions (predictive bash shell), authentication and user-level network services (when you have a predictable protocol).

    Q: how do you ensure errors in the speculative state don’t propagate to the main state? Need to be able to detect this, and could abort speculation in this case.
  • IDEA: Integrated Distributed Energy Awareness for Wireless Sensor Networks. A new “group diet” for wireless sensor networks. Problem of overloaded nodes. Existing solutions are “single node diets”, which are unsatisfactory because nodes have to collaborate. Local efforts cannot go far enough unless there is some cooperation. Aim to improve application fidelity by matching system load to availability. Shift load from overutilized to underutilized nodes, and shift load away from threatened nodes. Like a distributed OS for sensor networks. IDEA evaluates multiple solutions and distributes information to the nodes. Ideal goal is awareness of application constraints.

    Q: Quanto does some cross-node analysis? We’re building on these great ideas.
  • Flicker: Refresh Power Reduction in DRAMs by Critical Data Partitioning. Hardware is over-designed for correctness and reliability. Make it less reliable and tolerate errors in software. Smartphones are a motivation: power consumption is way too high, due to the use of DRAM for responsiveness. Battery drains even when a phone is idle. Goal is to improve power consumption here. If you increase the refresh cycle length, the power consumption drops, but the error rate increases. Currently use 64ms refresh, so could we increase this? Secret sauce is a partitioning into critical and non-critical (e.g. soft-state) data. Map critical data to short-refresh cycle DRAM, and non-critical data to long-cycle DRAM. Requires some hardware changes. Hypothesise that smartphones have a lot of non-critical data. Initial results show 25% drop in power consumption with only 1% loss in reliability.

    Q: [?] Looking at replication and checksumming in other work.
  • BFT for the skeptics. Industry deals with crash failures a lot, so do we need full BFT? We already use checksums, timeouts, sanity checks, etc. to translate faults to crash faults. How often do we get faults that require BFT to handle it? Looked at ZooKeeper and real-world failures. Yahoo!’s crawler uses ZooKeeper extensively. Saw 9 issues, due to misconfiguration (5, BFT wouldn’t help), application bugs (2) and ZooKeeper bugs (2, correlated, BFT wouldn’t help). Could BFT hurt? It has more things to configure, so misconfigurations could become worse. Need to show that BFT really solves a problem before industry will pick it up.

    Q: You showed that correctly implemented BFT couldn’t help with some failures? Failures were correlated, affecting all replicas.
  • Prophecy: Using History for High-Throughput Fault Tolerance. BFT has poor throughput. Need 3f+1 replicas to handle f faulty replicas. Can we improve this for read-mostly, internet workloads? Add a “sketcher” to each replica, which sketches requests and responses. Only one machine sends a full response, the others send sketches. Trades off consistency for performance, which gives delay-once linearizability. Faulty replicas can return slightly stale data. Internet services have unmodified clients and short-lived sessions. Look at performance of PBFT. Can improve by consolidating sketch tables on a trusted sketcher. We already trust middleboxes, so why not trust this too? Performance is much better than PBFT. Work not specific to BFT, and could apply to PAxos, quorums, etc. while getting similar benefits.
  • Securing Hardware Platforms Against Malicious Circuits Through Static Analysis. Make assumptions when building systems. Best way to break a system is to break its assumptions. People assume hardware is correct. What if we can’t make this assumption? Hardware is complex, expensive, static and the base of the system. Do “dead circuit identification”: highlight all potentially malicious circuits automatically. Attacker is motivated to avoid impacting functionality during testing (or else they’d be caught). DCI gets an assertion that says which paths are effectively short circuits. Use these assertions in a new graph algorithm to identify the possibly-malicious, dead circuits. No false negatives, but 30% over-identification. Empirical evidence shows a tight correlation between code coverage and

    Q: is this primarily at design-time on HDL? Yes, this is one of our assumptions.

    Q: what about redundant circuits for fault tolerance? This is used at design time where you can make calls about this.
  • Enhancing Datacenter Network Security and Scalability with Trusted End Host Monitors. Cloud workload is dynamic and hostile. Key selling point is that multiple tenants can share common infrastructure. Need a new approach to security, because exploits are more likely, and the cloud resources can be used to perform exploits themselves. Cloud datacenters can help: they are centrally-controlled so monitoring becomes easier. The software and hardware and homogeneous. Plus a clean-slate approach is possible. Use the hypervisor as a trusted component. Hypervisor can send alarms to central controller when an attack is detected. Built a prototype from Hyper-V and a trusted Intel NIC.

    Q: if you trust the VM, why do you need to trust the NIC? This gives some useful properties, and the NIC could do some filtering this for you.

    Q: HotOS paper on this exact topic?

    Q: [?] By “hypervisor” meant the entire virtualization stack, because we didn’t want to make the hypervisor itself any better.
  • Architectural Attacks and their Mitigation by Binary Transformation. What happens if someone tries to attack you from a VM on the same machine in the cloud. There is cross-talk through shared architectural channels. Example is contention for the CPU data cache. This leaks information about the memory access pattern, which could for example be used to leak AES keys. Have showed that EC2 has similar vulnerabilities: placement vulnerabilities, cloud cartography and cross-VM exfiltration are all possible. Approach is to use dynamic binary rewriting to transform x86 instructions so that the architectural effects are mitigated. Can degrade observation of timing, or inject noise and delays to hide leakage signal. Methodology is to make things secure by default, then come back to improve performance.

    Q: information leakage necessarily arises from statistical multiplexing, and we need statistical multiplexing to get good performance, so how can you address that? Assert that it should be possible.

    Q: how well would existing techniques protect against these attacks? Not aware of techniques that could do this.
  • Execution Synthesis. Say you have a bug in Linux on a remote machine. All you have to work with is a low-detail bug report. Reproducing it is time-consuming. Want a direction finding system from your system to a particular bug. Google Maps doesn’t do this at present…. So your bug report is a stack trace and some register contents. Do VM recording and replay. Don’t expect you to record behaviour that leads to the bug, since then you wouldn’t have the problem in the first place. Don’t care so much about performance, since you don’t run this in production. Find a state in the recording that is close to the bug report, then explore paths iteratively to get closer to the bug. Then you get a sequence of inputs that lead to reproducing the bug. Need a distance function, way of choosing inputs, and good information about what to include in a bug report.

    Q: could you go backwards from a failure state and execute in reverse? We don’t have the entire failure state to begin with.
  • Edge Mashups for Clinical Collaboration. Health industry is going from paper-based to electronic records. Want to empower non-programmers to build applications for real-time collaboriation, but need to respect things like HIPAA for logging and data retention. Example use-cases include expert-assisted surgery (call an expert for advice when complications arise, in real-time), and micro-clinics where nurses see the patients, but doctors write prescriptions remotely. Envision a graphical tool that pulls in photographic and chart data, which is synchronized between all participants. State serialized to XML which can be distributed to all the clients. Could be client/server or peer-to-peer. Need logging for accountability. “Break-glass” access control: anyone gets access but they are held accountable after-the-fact. Need low latency so doctors don’t feel that they are wasting time. Might migrate this to the cloud for scaling.

Kernels

seL4: Formal Verification of an OS Kernel

  • Formally proved the functional correctness of 8700 lines of C. No bugs.
    Want to build high-assurance systems: small kernels which reduce the trusted computing base. Want strong security properties. Kernel has to be correct: if it falls over, so does the whole system.
    seL4 has capabilities.
  • Proof is that specification and code are equivalent. Need a formal semantics for every system call. Use Isabelle as a theorem prover to bridge the gap between spec and code. But what about assumptions (in the code) and expectations (of the spec)?
  • Assume correct: compiler and linker, 600 lines of assembly code, hardware, cache, TLB management and 1200 lines of boot code.
  • Given these assumptions, we get some nice properties: no null dereferences, no buffer overflows, no code injection, no memory leaks, no div-by-zero, no undefined shift, no undefined execution, and no infinite loops or recursion. Does not imply security, lack of bugs from expectation to the physical world, or absence of covert channels.
  • Proof architecture admits proofs of higher-level properties (e.g. access control).
  • Design is written in Haskell, which can be used to generate Isabelle code automatically.
  • System model has three states: user, kernel and idle. Events are syscall, exception, IRQ and VM fault.
  • Call graph is messy! A microkernel takes all of the messiness and packs it into a very small space.
  • Formal methods practitioners (fans of abstraction) versus kernel developers (exterminate OS abstractions). Different view of the world. Haskell prototype unified these two things: OS people got to implement an OS, while the formal methods people got well-defined semantics. The C code is manually-written and hand-optimized, but based on the Haskell prototype.
  • Aim to reduce complexity. Have to deal with virtual memory in the kernel. But we can put drivers outside the kernel. Concurrency is complex, so use an event-based kernel and limit pre-emption to a few well-chosen points in long-running operations. The C code is derived from the functional representation. Need to support a subset of C: everything from the standard, minus goto, switch fall-through, & on stack variables, side-effects in expressions, function pointers and unions.
  • Found 16 bugs during testing, and 460 bugs during verification (roughly equally distributed between the C code, the design and the spec). Took 25 person-years in total: $6 million (compared to $87 million for EAL6).
    One of the largest proofs ever done in a theorem prover: 200kloc handwritten, machine-checked proof. Proved 10kloc of OS code.
  • Q: can you comment on what happens when you have to evolve the code? What effort is required? It depends. An optimization on the code level that doesn’t change the semantics might need a few days to re-prove. A new feature that adds new components could be added (in the paper) doesn’t depend on the rest of the kernel as long as you don’t screw around with existing data structures.
  • Q: does your work solve the stated problem? The assumptions are significant, and you’ve just done a very significant type-check on the code? Is it really possible to solve the originally stated problem? This is just the first step. You can reduce the assumptions with more work. It isn’t the only technique that you should use, so if you deploy it in an Airbus you should also do testing and verification. [Taken offline.]
  • Q: how can you verify something high-level like having the address spaces of two processes being isolated? We do this. You can still use seL4 in a stupid way, but you can use our security model with capabilities and reason about those in the spec. You don’t have to go down to the code.
  • Q: did you see a correlation between the logical errors in the specification and the implementation? Not really. The C bugs were fairly “stupid”: typos, copy-and-paste, etc.
  • Q: wouldn’t it be better to prove temporal properties? Are they expressible? They are expressible. We look at functional correctness, not temporal properties. But you need functional correctness before you can reason about temporal properties.

Helios: Heterogeneous Multiprocessing with Satellite Kernels

  • Systems are getting more complicated, from UP to SMP to CMP to NUMA. This is still homogeneous. But hardware is no longer homogeneous: programmable NICs, GPGPUs, etc. Operating systems ignore this heterogeneity: the other devices have different instruction sets and often no cache coherence. This means that the standard OS abstractions are missing, and programming models are fragmented. Can we bring this back into the operating system?
  • Helios is an OS for distributed systems in the small. Use four techniques to manage heterogeneity, simplify app development and provide a single programming model for heterogeneous systems.
  • Result is that it is possible to offload processes to these heterogeneous devices with no code changes. Also improves performance on NUMA architectures.
  • Satellite kernels. Want to make use of an I/O device, but the driver interface is a poor interface for applications that want to use programmable devices. It becomes hard to perform tasks like debugging, I/O and IPC with these devices. The driver doubles as an OS, within the OS itself. A satellite kernel runs on the device itself: fundamentally a microkernel. Also run separate satellite kernels on each NUMA node. Local IPC and remote IPC for communication between satellite kernels.
  • Applications register as services in a namespace. The namespace connects IPC channels.
  • Application placement is constrained by the use of heterogeneous ISA, an expectation of fast message passing and platform preference. Applications are allowed to specify affinity in their metadata: a hint for where the process should run. Easy for a dev, admin or user to edit affinity. Platform affinity is processed first, and this gurarantees certain performance characteristics. Can also contra-locate, e.g. if you don’t want the interference of an anti-virus program running on the same core. Algorithm attempts to balance simplicity with optimality.
  • Applications are first compiled down to MSIL, and then that is compiled down to the appropriate ISA. Can encapsulate multiple versions of a method for different ISA in the MSIL (e.g. fast vector math).
  • Implemented on Singularity, using an XScale programmable I/O card (2GHz ARM processor with 256MB of DRAM). Just need a timer, an interrupt controller and the ability to handle exceptions to implement a satellite kernel for a new device. No need for an MMU (thanks, Singularity!). GPUs are adding timers (Larrabee). Only supports two platforms and a limited set of applications.
  • Evaluated several applications (network stack, FAT32 FS, mail server, web server, etc.) and how easy it was to run them on satellite kernels. Almost no code had to be changed (only in the TCP test harness). One line of metadata had to be changed in almost every case (zero in the other).
  • Offloaded an entire networking stack to the XScale, and showed that the end-to-end performance of PNG compression-and-serving is improved when offloading to the XScale.
  • Considered an email server built on Singularity, using a NUMA box. Emails per second handling improved by 39%. Turned out that the instruction throughput was much higher due to better cache utilization.
  • Q: when you transfer data between two NUMA domains, couldn’t the IPC fail due to memory allocation failures? Singularity is statically verified, using contracts, so we don’t have to worry about that.
  • Q: is this not just 20-year-old distributed microkernel research rehashed? We pay homage to that in the paper. A simple heuristic is sufficient to decide where to run some process, and you need to have process migration anyway, so why not just use that when you get a problem? Process migration is pretty difficult, in the heterogenous case. Abstraction turned out to be pretty brittle in commodity OSs.
  • Q: is it reasonable to rely on protection from a large runtime? The system isn’t dependent on type-safety.

Surviving Sensor Network Software Faults

  • Sensors have to operate unattended for months or even years. It’s hard to debug failures considering that the input is unknown. There is no debugger.
  • Safe TinyOS introduces memory safety to sensor nodes. But what do you do when you get a safety violation? In the lab, spit out an error message; in the wild, reboot the entire node (losing valuable soft state and application data).
  • Neutron is a new version of TinyOS. Reduces the cost of a violation by 95–99%. It has near-zero CPU overhead during execution. Runs on a 16-bit microcontroller.
  • A TinyOS program is a graph of software components: statically instantiated code and state. Connections are typed by interface and there is minimal state sharing. Now have preemptive multithreading with a non-blocking, single-threaded kernel. Aim is to separate the program into independent units for recovery. Infer the boundaries of these at compile time. The kernel is a single unit.
  • Units can be rebooted independently. A wrinkle involves cancelling system calls, so you need to block if a syscall is still pending. Blocks of allocated memory are tagged with the owning recovery uint, which enables these to be freed on reboot (by walking the heap). Can even reboot the kernel: just cancel all pending system calls (return ERETRY), and just have to maintain thread memory structures. Applications will continue after the kernel reboots.
  • New idea of “precious state”: a group of precious variables will persist across a reboot. Annotate variables in the source code. Some restrictions on precious pointers. Precious variables must be accessed in atomic blocks. Variables are persisted on the stack across reboot: the set of precious state is usually smaller than the worst-case stack size.
  • Evaluated the cost of a kernel violation in Neutron, compared to safe TinyOS. Looked at three libraries, running on a 55-node testbed. Show the effect of a reboot on the CTP workload. Neutron gets close to the non-reboot case. Also look at the effect on time synchronization in FTSP, showing what proportion of the nodes have unsynchronized time. Again, Neutron gets close to the non-reboot case. Looked at fault isolation. CTP and FTSP data persist across reboots.
  • Main cost is in ROM bytes: 1–5kB of added code, roughly constant.
  • Measured cost of a reboot in milliseconds. A kernel safety violation will result in a 10–20ms outage.
  • Much lighterweight than microreboots (and lets you reboot a kernel, not a J2EE application).
  • It’s easy to change the TinyOS toolchain, but changing the programming model isn’t due to the amount of deployed code.
  • Q: how can I reason about a node that has survived a fault (a rebooted node is in a known-good state)? Do you have evidence that this is going to help us? [Showed emails from the questioner.] It is hard to diagnose these faults. Different approaches are possible.
  • Q: what do you think of the alternatives, such as using an MMU, verification or simulation? Well we could add an MMU, but we don’t have it at present. These new developments might make the dependability better. Verification struggles with the huge input space.
  • Q: how do you ensure that the precious state is not corrupted? Using safe TinyOS, so we won’t see memory access violations due to memory safety. Taint in the paper is about inconsistent state, not corruption.
  • Q: what are your criteria for what state should be marked as precious? Don’t have a strong set of guidelines for this, but have done it by inspection so far.
  • Q: what is your fault detection system, and what is its coverage? How do you know when you have a fault? The deputy compiler gets you to annotate code with things like buffer lengths. Can infer faulty behaviour from these. Annotating interfaces tends to be sufficient.
  • Q: this is a very valid approach?

Leave a Reply


suboxone and buspar strattera drug dosage buy cialis delivery valtrex generic dose doxycycline renal adjustment astrazeneca nolvadex 10 mg propecia 1mg us cialis 12 mg cialis generic costco cheapest cialis drug lexapro 5 mg bula efeitos viagra 50mg 90 mg of buspar buying viagra indonesia cipro dosage use prednisone burst 200 mg hydrochlorothiazide tablet ingredients nexium 40 mg image budapest cialis price indian viagra suppliers drug information metformin condition prescription clomid green viagra 3800 mg buspar racing heart price synthroid walmart nexium low cost discounted 36 hour cialis celebrex drug patent cipro torn meniscus buspar stop smoking clomid 50 mg bodybuilding cialis muscle spasms generic levitra mg efekti tablets viagra buy propecia rx finesteride versus propecia prospect celebrex 100 mg pfizer zithromax buying viagra shanghai levitra us sales pediatric augmentin suspension celebrex target wellbutrin 600mg cheap cialis usa purchase xenical orlistat nolvadex usa price indian cialis ripoffs nexium pills dosage priligy pille kaufen cialis fc cyprus vademecum cialis 10 mg forum generic cialis cipro sleeping pills strattera dosage cost cialis without prescription getting lexapro online 1000 mg glucophage xr cheap viagra prescription 600 mg wellbutrin xl cialis red pills viagra price durban generic viagra caverta amoxil online buy cialis dosage 60mg clomid shop uk viagra prescription coverage tinitus from cialis lisinopril 20 mg hydrochlorothiazide augmentin tablet dose levitra sale viagra cost propecia uk viagra plane tablets zovirax suspension vademecum propecia causespremature ejaculation 5mg cialis discounts costco generic diflucan cheapest viagra super strattera nausea drug information lasix bactrim online uk generic lexapro walgreens buy periactin celebrex discount coupons buying clomid australia doxycycline cause hemorrhoids bactrim ds 2 tablets nexium mups tablet buying 800 mg viagra zovirax tablets sale kamagra kautabletten 100mg price propecia philippines kamagra usrbiji zoloft 1000mg generic cialis online buspar liquid form nome generico bactrim acquisto viagra generico buy nolvadex pharmacy 2.5 mg lexapro reviews discount viagra onlilne diflucan 2mg cialis related drugs pertes sous clomid xenical 120 mg nr.21 levitra canadian generic cialis 10mg dose ordering nolvadex online 10mg prednisone 4 time viagra femenina online sertraline zoloft 100mg metformin simvastatin together nolvadex tablet colors kamagra buy uk celebrex street drug nexium 40 uses viagra cost costcol propecia online 1.25 mg order prescription propecia valtrex quanto custa tesco viagra prescription zovirax cheap viagra prescription medicine viagra covered religious viagra online legal cialis daily usage wellbutrin sr skusenosti order cialis sydney nexium cost australia kamagra shopping uk buspar 90 mg daily order doxycycline 100mg zoloft 1 mg nolvadex clomid australia glucophage foglietto illustrativo erythromycin pill reviews clomid 100mg tips lexapro generic canadian levitra pharmacy dublin cytotec uso veterinario viagra tesco online clomid without cycle purchase zovirax tablets generic cialis 200 mg viagra pfizer coupons buy kamagra california cipro 1000mg xr celebrex users forum generic cialis switzerland kamagra uk shop viagra philppine price amoxil 500 mg bestellen cost for celebrex glucophage 850 mg price nexium cause dizziness viagra buy japan buspar symptoms buy cialis Washington zithromax 600 mg price cheap viagra herbal clomid prescription medicine europe generic viagra oral propecia cost zoloft 150 mg tablet lisinopril price uk buy viagra prof augmentin 1000 mg ulotka lexapro become generic nolvadex 10mg ed can buy priligy diflucan prescription only zithromax capsules 250mg cialis malaysia online generic alternative nexium increased nervousness zoloft lupin generic zoloft price zovirax france 25mg viagra young buy viagra canadian 100mg clomid days 5 9 doxycycline dosage 75 mg mayne doxycycline 100mg wellbutrin party drug generic strattera price bestlife generic viagra 150 mg zoloft dosage clomid 100mg cost cialis sale australia viagra man costumes doxycycline hyclate buy clenbuterol viagra dangerous breaking cialis pill viagra 25 mg generic lexapro tablet size viagra canadian pharmacy usa viagra prescription erythromycin cost uk prednisone deltasone 20 mg amoxil capsules uses bactrim forte 480 mg cheapest generic celebrex clomid 5omg viagra and superdrug augmentin generico mylan nexium enterotabletter bayer house levitra phenergan cause nausea viagra online malaysia doxycycline genrx price propecia tablets discount levitra tablets generic chinese cialis lasix rxlist forum propranolol 40 mg usa made viagra buy clomid uk. celebrex alternative drugs house manufacturer nolvadex m b3 555 buspar buy cialis france genericos de viagra lisinopril 12.5 pharmacy lisinopril 10 mg images wholesale viagra paypal 40 mg of buspar clomid 50 mg posologie viagra pfizer bd viagra generic now viagra prices list generic levitra work buy viagra authentic celebrex 100 mg indicaciones buying viagra switzerland 25mg viagra price using liquid viagra discount coupons cialis 20 mg cialis dose generic kamagra australia nexium prospect 20mg augmentin 375 used for prescription de cytotec lisinopril al 20 mg zdravlje prednisone tablete buy Cialis 120 Tabs online clinic cialis zovirax order canada order xenical medicine cheapest priligy uk usos del metformin synthroid 112 mcg price levitra rezeptfrei kaufen strattera drug contraindications propecia tabletes clomid 50mg tablets strattera 4 mg levitra 20mg 8st depression sous clomid achat clomid 50mg illegal viagra uk metformin causing heartburn augmentin discount coupon celebrex coupon canada doxycycline buy dosage propecia causes sterility clomid 50mg follicles xenical 120 mg bestellen lisinopril generic appearance zoloft e menopausa metformin cost cvs generic cialis polska levitra uk cheapest lexapro 30 mg pregnancy zovirax order lipactin cheap viagra rupees erythromycin 250 mg dose wellbutrin causes tinnitus 500mg valtrex uses cialis australia laws buy celebrex usa usa 800 mg viagra doxycycline untuk 40mg levitra danger viagra generic version nexium 40 mg capsules medicament prednisone 20 mg purchase 60mg cialis autoimmune prednisone uses generic zoloft alcohol legal canadian viagra buspar 5mg malaysia cialis online 5 mg lexapro usage cialis 5 mg opinie vendita levitra generico viagra soft cheap overnight viagra pills nolvadex illegal us cipro cause acne nexium iv infusion valtrex generic effectiveness buy kamagra cialis propecia tables uk pastilla lisinopril 10mg. zithromax online canadian cialis online consult buspar amphetamine effexor buspar interactions levitra 5 mg kullanimi clomid causing gas viagra generic drug nolvadex australia forum buy viagra philipines 3 day 10 mg prednisone buspar and elderly viagra pfizer overnight zoloft causing mania split viagra pill indian viagra 100 doxycycline 100mg syphilis wellbutrin flushing cipro renal adjustment zovirax australia strattera the drug generic levitra reviews erfahrung cialis 5 mg vaginal bactrim uses cialis 20mg vierteln buy 200 mg viagra propecia dosage 0.25mg buying doxycycline online prednisone 10 mg online buy lisinopril hctz prednisone uses rash bactrim price buspar and adderall cialis 10 mg erfahrungen zoloft purchase canada viagra ausprobieren lexapro 10 mg citalopram nolvadex tamoxifen tablets price viagra pills propecia brand buy user reviews zoloft 10 mg cialis cost kamagra for us uso prolongado xenical trustworthy generic cialis amoxil amoxicillin sale purchase cialis usa cipro 500 used for generic cipro 500mg lisinopril 12 mg viagra price manila cialis 20 mg price levitra 20 mg wholesale nexium go generic cialis discount online lexapro muscle growth bactrim pill size uk kamagra risk doxycycline 500mg tooth 40 mg cialis pills buspar settlement buy lasix 500 mg push lasix slowly clomid and muscles starting lexapro nausea get viagra generic zoloft bula 50mg cialis generic jakarta 20 mg doxycycline buy usa viagra kaufen valtrex generic dosing levitra basso costo purchase legal clomid tinnitus and lexapro genaric viagra pills doxycycline pill contraceptive cheap online diflucan cipro 20 mg augmentin for sale tetracycline 250mg cap zithromax 250 mg preis order lasix online drug interaction valtrex muse viagra together drugs like zoloft lexapro causes aggression nhs viagra cost to get cialis 20 mg buspar cialis cost low valtrex used for strattera exhaustion use viagra tablet couples using viagra buy canada viagra pregnancy using viagra viagra generic soon cipro 250 mg price cialis take 2 5mg zithromax 500 mg image periactin foglietto illustrativo strattera generic available buy strattera usa nolvadex pct purchase bactrim pillola anticoncezionale kamagra online canada prednisone 10mg online viagra canada echeck cialis e ictus prednisone cause anger prednisone 20 mg cvs hydrochlorothiazide tablets used neveda viagra prescription bactrim suspension peds wellbutrin abilify together lipiblock generico xenical doxycycline 100mg mp 37 diflucan sciroppo 50 mg zovirax suspension generic phenergan 25mg tablets forums generic viagra doxycycline 200 uk buy generic 80 mg lasix tetracycline canada online buy diflucan express cialis generic 200 mg viagra prescription criteria metformin generic 850 mg rx viagra generic cialis pills 2.5 mg wellbutrin robitussin interaction zoloft da 100 mg their generic lexapro 200 mg zoloft online cialis purchases purchase viagra professional zithromax dosage prescription buy generic celebrex diflucan pill information amoxicillin versus erythromycin levitra 20 mg 4 tablet doxycycline 100 mg shortage buying celebrex online propecia online fake zithromax price comparison bayer leverkusen levitra zithromax dose sinusitis viagra thailand customs propranolol bula 40mg cialis generic daily celebrex use arthritis xenical 120 mg priser vilazodone versus zoloft low cost lexapro buspar 6 weeks cialis user experiences levitra massachusetts cipro stomach virus 150 mg of clomid viagra prices au compra buy doxycycline target pharmacy cipro prednisone bigger muscles indian viagra problems phenergan ativan together cialis tablets 10 mg cialis 40mg doxycycline and haemophilus lexapro psychotropic drugs xenical online usa rusu gruppe viagra cheap levitra 20mg buy viagra caverta taking buspar buying clomid 150 mg zovirax suspension storage zoloft wellbutrin buspar cialis kaufen niederlande cialis 5mg tetimonials zoloft tablete nuspojave viagra other use viagra 100mg effect viagra red 200mg doxycycline cause bumps synthroid generic buy uso medicamento zoloft generic viagra listings viagra wholesale paypal drug testing viagra bangkok generic viagra valtrex rx 905 kamagra 100 brausetabletten lisinopril 10mg petunjuk penggunaan cytotec generico cialis foro synthroid cost canada 900 mg zoloft generic viagra benefits prednisone generics cytotec yliannostus viagra cheap usa street price levitra 20 propecia cost canada nexium causes headaches 175 mg synthroid potenspiller cialis doxycycline 50mg dogs ip 272 pill bactrim zoloft users metformin causes acne viagra 100 mg canada xenical 120 mg 252 kaps. clomid 100mg headache levitra price 10 mg cheap prescription propecia buy viagra scarborough buy finasteride propecia cytotec mejor uso lisinopril anxiety disorder propranolol 40 mg tabletki clomid rx online prednisone crushed erythromycin gel cost zoloft causing tremors zoloft nervous stomach clomid 50mg cm wellbutrin 300 mg xr diflucan dosage intravenous costo xenical metformin smaller pill diflucan untuk viagra pricing 50 mg cialis 5 mg tadalafil buy nolvadex information 2012 tesco pharmacy viagra periactin 4 mg tablet levitra 60 pills online cialis 20 mg gr prednisone lose muscle hydrochlorothiazide tablets india clomid 50mg prescription zithromax 4 capsules uk staphylococcus aureus augmentin buy wellbutrin cheap lisinopril without prescription wellbutrin generic ok buspar buspirone dose viagra pillen testen diflucan cps 150 mg propecia without subscription viagra in anus levitra usa kaufen arch house cipro buying online viagra comprar viagra 25mg propecia 1 mg t viagra australia melbourne cheap dubai viagra canadian viagra ads buspar works instantly cialis online 5mg viagra 100mg buying costo zovirax compresse 1 viagra tablette kaufen buspar opiate withdrawal viagra generic customs lexapro cost target buspar stomach buy cream viagra doxycycline inducible lentiviruses lexapro 10mg or 20 buy cialis levitra cialis 5mg n3 viagra 25mg tablet celebrex sulfa drugs cialis prescription voucher pussy with viagra online propecia consultation cost of nolvadex indian viagra london 2.5 mg cialis cost viagra us canada buy doxycycline 150 mg propranolol without rx lisinopril 20 mg take dosage zovirax pills augmentin antibiotic nausea mylan lisinopril 2.5 mg prednisone tinnitus worse purchase viagra japan tetracycline citrus cialis 40 mg review cytomegalovirus valtrex kamagra order caverta image lasix pill zovirax tablets tablets tableta nolvadex shqip ukmeds4u viagra thyroid drug synthroid levitra drug insert nolvadex 10 mg tab zoloft angustia buy zovirax 200 levitra 20 mg uses buy prednisone line zovirax tabletten 400 harga nexium 10 mg price lexapro 5 mg cialis costs uk doxycycline suspension dose prednisone 5mg posologie buspar pi sheet 37.5 mg of zoloft cialis 100 mg fiyat propranolol causes anxiety viagra pills generics fish doxycycline uk lasix causes hypokalemia diflucan szuszpenzio nolvadex pills online generic cialis. xenical uk synthroid australia viagra pills color kamagra direct uk prices levitra 5mg buy levitra calgary clomid generic vs hard without levitra cialis in brussels propecia online overnight augmentin 500 mg antybiotyk levitra drug action clomid 0.1 mg viagra forums australia herbal cialis australia cheapest 10mg cialis valtrex best prices cialis jelly 20mg 20 mg cialis cheap viagra 100 mgs cost zoloft 50 or 100 mg buy levitra paypal prednisone eg 5 mg italy viagra price cipro cause bloating viagra drug prescription viagra 100mg rating cytotec abort tabletter generic lexapro symptoms generic medicines viagra tetracycline no prescription losartan hydrochlorothiazide 50 mg metformin generic names doxycycline hyclate order propranolol de 20 mg xenical 60 india price buy nolvadex aus buspar help ocd xenical indian cost uses of amoxil 500 lasix 40mg strattera cap 40mg levitra 10 mg italiano xenical 200 mg bilgi propranolol without prescriptions viagra 100mg pey buy cialis auckland cipro cause indigestion buspar helps me buspar brand name lisinopril 2.5 mg hypertension viagra 500mg uso ja usei cialis viagra online acquisto generic viagra deals zoloft versus sertraline periactin used for augmentin type drug prednisone 10 mg bronchitis cvs 5 mg cialis viagra sale 25mg viagra use paypal effets cialis 10mg viagra usa 800 mg valtrex from india strattera mgs augmentin causa candida buy cialis johannesburg cytotec ve abortus synthroid 0.088 mg bayer levitra 5 mg generic viagra china generic viagra busts bactrim philippines price women viagra buy cialis phone orders buspar cannabis buying viagra forum buspar and sudafed buy nolvadex 40mg 1 cycle sous clomid zoloft muskelschmerzen xenical 120 mg drug metformin pills viagra prescription card augmentin drug label cialis de 100 mg levitra schmelztablette nebenwirkungen brand cialis 2.5mg buy viagra generic free kamagra tablets synthroid ou generico lisinopril dosage cost prednisone 10mg com zovirax 50 mg blue valtrex pill letrozole versus clomid erythromycin 250 plus 20 mg levitra propranolol forgetting drug viagra used daily cialis 100mg sydney viagra walmart cost lexapro 10mg appetite kamagra 150mg doses cialis 50mg kaufen phenergan plus 2 levitra prescription buy online zoloft viagra kaufen stuttgart price of synthroid cipro drug company buspar faq viagra in austin viagra prescription price miconazole versus diflucan cialis continuous use kamagra.com uk buspar thyroid buy nolvadex gyno clomid inofolic plus identify metformin 500 mg synthroid 125 prices diflucan jedna tableta cost cialis algodones cialis 2.5 mg appearance paypal cialis online use viagra wiki buying cialis budapest buy viagra 100mg mg doxycycline uti drug testing clomid Cialis 5 mg Washington levitra cut pill there generic levitra wellbutrin 450 mg benefits strattera free prescription erythromycin ethylsuccinate 500 mg propecia buy london canadian online viagra doxycycline tablet kullananlar diflucan compresse 150 mg cialis tablet kamagra kaufen lastschrift cheap brand cialis the indian viagra levitra canada drugs strattera 18 mg pret cipro 500mg bula split valtrex pills snort cialis 20 mg dubai prescription cialis generic propecia cost viagra canada forum cialis retail cost nexium 20 mg 14 tab zoloft versus prozac emergency valtrex prescription nolvadex vs generic viagra buyer usa doxycycline causing reflux viagra prescription pill viagra pfizer france xenical 120mg philippines lexapro 20mg gotas viagra cialis kaufen buspar anger levitra go generic kegunaan doxycycline tablet cialis generic 20 doxycycline 100mg opinie cut cialis pills abilify buspar interactions viagra blu 800mg nexium 10 mg brasil compare viagra price augmentin 500 mg tablet buspar epilepsy lexapro 20mg engorda buspar and strattera pfizer herbal viagra generic valtrex pills diflucan otc canada australia viagra otc experiences using zoloft daily cialis prescription first use viagra buy metformin mexico acheter pfizer viagra canadian viagra email cost viagra tijuana prednisone 1mg qualitest doxycycline muscle stiffness 20mg cialis double viagra buyers canada 6generic propecia effective buspar hypomania cialis 5 mg costo synthroid price cvs generic clomid 50mg prednisone dosage 30 mg zoloft prescription canada metformin price walgreens cialis online canadian viagra india reviews amoxil 250 mg tablets kamagra gold buy viagra haittavaikutus price levitra costco tetracycline canadian pharmacy propranolol cause hyperglycemia erythromycin al 500 filmtabletten lisinopril 40 no prescription buspar plus ssri 2 diflucan pills makes generic synthroid viagra 150 mg purchase zoloft sertraline 50 mg cialis cheapest cialis 5mgcenik lexapro price drop viagra generic in 2012 xenical users forum augmentin 1000 mg alkol synthroid and confusion doxycycline tablets 100 mg 6 cheap propecia online phenergan drug screen cialis cost kaiser costo cialis 20 mg levitra generic 10mg drug information cipro levitra billig kaufen buspar lexapro klonopin show pill viagra cost of priligy celebrex prescription card prescription to propecia viagra strips uk nexium 20 mg pakkausseloste almus doxycycline order nolvadex forum costco pharmacy metformin generic valtrex 1000mg clomid costs uk lisinopril scored tablet priligy drug viagra hyderabad buy buspar sustained release erythromycin sebaceous cyst lexapro generic when pfizer egypt viagra viagra canadian patent nexium in uk cialis brasilia buy zoloft depression drug cialis 100mg pills generic valtrex expensive prezzo cialis 5mmg doxycycline versus zpack kamagra india delivery cialis dose rxlist walmart prices levitra cialis 20 mg tabletas buy strattera 25 mg doxycycline 100mg tablet metformin white pill priligy 30mg buy ebay diflucan pill lisinopril generic sale lexapro discount lasix 40 mg tabletki drug classification strattera cheap dapoxetine uk synthroid medication cost wellbutrin causes tremors viagra pills free generic viagra ert 100 phenergan type drug doxycycline mono 50mg cytotec 200 usage 100mg viagra paypal propecia augusta buy buspar online kamagra flushing strattera no prescription generic synthroid rash metformin getting pregnant clomid challenge borderline bactrim drug category cialis discount prescriptions walmart cost cialis thuoc hydrochlorothiazide 25 mg cost viagra alternative bactrim herx levitra 1 omg cheap viagra germany propecia canada prescription generic lexapro india erythromycin acne mg 50mg kamagra safer buy cipro zithromax 50mg viagra sale propranolol pill sizes cipro drug manufacturer australia cheapest viagra 100 fake prescription viagra lisinopril causes headache buy viagra site muse plus levitra price nexium cipro denk 500 tablets online doxycycline 100mg cialis 10mg canada alli orlistat costs tabs clomid synthroid 75 mg bula diflucan candida krusei buy clomid discount zoloft generic drug bactrim antibiotic use wellbutrin and menopause viagra 100 reg price cialis shipped us zovirax labiale uso india viagra cipro certified pharmacy viagra augmentin sulfa drugs viagra price india synthroid 100 mg cost buying viagra inline diflucan 150 mg alcool bactrim f 800 mg generic wellbutrin 300xl buy real levitra nexium 20 mg preis kamagra plus wirkung visiting india viagra buspar zaps harga nexium generic synthroid 75 mcg cost foro levitra 20 mg levitra 10 mg halbieren generic cialis rating xenical online clinic xenical kaufen online order cialis Washington viagra india lequid lexapro nausea drowsiness sustanon 250 propecia sale valtrex nexium 20mg tabletten single use viagra buy nolvadex buy lisinopril tablets prescribed 2 viagra pills together cheap clomid pills bactrim tablet 800 viagra ou generico cialis online au clomid 500mg cialis cost uk generic 5 mg levitra levitra tabletta lisinopril drug brochure nexium 10 mg powder posologie diflucan 200mg metformin order levitra kaufen nachnahme costof viagra levitra flushing kamagra now online ordering lasix viagra purchase switzerland strattera 25 mg atomoxetine buspar category b 8000 mg viagra reviews cialis mg 10 zoloft nausea help lasix medlineplus metformin dosage 500 mg valtrex walgreens price lasix use bleeding 50 mg clomid pct levitra cupon online propranolol miracle drug cipro 250 mg fiyati viagra professional uk cipro 500 mg antibiotics amoxil buy online buying viagra generics zovirax suspension preis two 5mg cialis tetracycline kaufen tabletki odchudzajace xenical zovirax walgreens price viagra exhaustion cialis india prescription viagra india shopping sinusite bambini augmentin frequency prednisone use glucophage 800 mg augmentin 650 mg prospect 5 cialis generico sildenafil viagra kaufen kanada stewarts pharmacy cialis wellbutrin online kaufen generic viagra 25mg bactrim tabletki dawka 5 mg cialis price cialis use tagalog prednisone withdrawal nausea glucophage tablets 1000 mg zithromax 250 price generic synthroid lannett cialis free tablets nexium generic usa propecia canada 5mg viagra versus levitra levitra order overnight buy viagra cheaply augmentin bustine 1 mg price of 10 cialis valtrex buy generic cialis 20mg billig uk propecia tablets any indian viagra vegetal viagra 200mg buspar hedweb cialis 5mg canada prednisone tussionex medco propecia 1mg hexabotin erythromycin 500 mg propecia walmart canada acne cause propecia cialis without insurance online recept viagra zovirax tablets diarrhea cialis 5 mg 20 mg zoloft causing aggression orlistat generic xenical cialis toronto order propecia merck cheapest buying cialis australia tetracycline kapsul 500 mg cialis 5mg brand ritalin strattera together buy kamagra amsterdam amoxil 250 mg pregnancy wholesale kamagra uk 100 mg red viagra uso cialis 10 mg cialis pro canada uk free viagra target propecia cost clomid tablets uk buy viagra ottawa suscribe mailing viagra wellbutrin xl discount cialis preis usa enterococcus species bactrim zithromax 250 mg n1 drugbank metformin kamagra verkaufen strafbar order amoxil online clomid ile mg monthly cialis cost buy weekend viagra buy propecia coupon cialis contraindications use sale viagra liquid kamagra jelly order prednisone 15mg take 1000 mg valtrex 0 5 mg propecia posologie cialis 20mg zithromax 1 gm price use lasix medication lexapro is dangerous cialis kaufen thailand buy online propecia generic wellbutrin 150 mg metformin hyperinsulinismus 5 mg cialis australia generic viagra for .72 viagra sushi roll bijsluiter kamagra 100mg generic viagra california augmentin online canada identify viagra pills drug doxycycline 100mg erythromycin diffuse panbronchiolitis cialis malaysia buy generico nexium 20 mg wellbutrin versus seroquel cytotec 0.2 mg misoprostol lisinopril hydrochlorothiazide price kamagra kaufen expressversand clomid drug test 50 mg diflucan prednisone tight muscles prednisone 2.5 mg information clomid en cyclus generic lexapro walmart propecia causes anxiety viagra online discount cialis 3800mgx 10 pills cosa costa cialis propranolol tablets 80mg generic viagra ingredients 2 25mg of viagra drug lasix used 200mg kamagra doxycycline hydrochloride 100 mg viagra costs insurance doxycycline vibramycin cost zoloft 50 mg high bactrim sulfa drugs harga doxycycline 100 mg cipro online registration viagra em manaus 4 mg prednisone canadian generic nexium valtrex price australia kein samenerguss cialis cialis 150mg generic levitra target brand zoloft price cialis 10 mg directions valtrex prescription drug metformin nebenwirkung haarausfall nexium jeuk prednisone muscle tear costo viagra 25 mg vand viagra generic augmentin 500 suspension buvable viagra 50mg efeito cialis line order buy clomid generic cipro 500 mg tablets prized viagra online pfizer cialis 100m buying valtrex canada price cialis india augmentin drug contraindications lasix 100 mg erythromycin 400 mg acne diabetes insipidus prednisone zithromax 1000 mg uses 100 mg clomid cyst propranolol sdz 10mg buspar online kaufen cialis cheap uk tesco viagra price 2013 cipro 55 for sale erythromycin sinusitis dosage cheapest 1 mg propecia celebrex vs generic viagra generic quality Cialis 20mg 20 Tabs xenical dosage uk viagra prices krogers celebrex causes rashes cialis generic worldwide lexapro drug name viagra tablets cost metformin 500 mg uses chewable viagra 100mg generic augmentin prices doxycycline caps 100mg 14 panafcort prednisone 25 mg kamagra viagra buy viagra online order when viagra generic 120 mg lisinopril overdosr viagra gold australia propecia tablets ireland generic nexium coming cipro dose sinusitis prescription drugs lasix viagra 30 tablet xenical bagus ga augmentin 625 mg tab dragonflies pills viagra viagra 200mg erfahrungen generic viagra co order clomid prescription order generic viagra nexium and flushing lisinopril 5 mg tabs cheap generic synthroid online kamagra australia is viagra injurious synthroid prices usa wellbutrin sr100mg tetracycline 500mg used propecia tablet advantage zovirax 200mg cena buspar 10 mgs zoloft online uk order natural viagra to buy periactin phenergan drug facts order viagra cvs augmentin tabletas dosis iui without clomid propecia price viagra comanda online cialis cost mumbai shop cheap viagra buy cialis sublingual augmentin generic price purchase viagra now buy lisinopril london wellbutrin xl 150 mg augmentin causing insomnia pfizer turkey viagra cytotec australia cialis generic 50mg buy bactrim generic celebs using propecia metformin price walmart reichen 5 mg levitra uk viagra chemists generic viagra buyer generic levitra tablets cialis 2,5mg paypal price levitra usa order strattera online Cialis Professional 20 pills getting off metformin generic metformin manufacturer 50 clomid tablets uk buy celebrex pfizer propranolol causes palpitations levitra schmelztabletten 20 mg generic viagra uk. prescription required cialis usa viagra 100 enterococcus treatment bactrim buspar potency canadian viagra dangers viagra online overnight kamagra 100 mg sobres celebrex 200mg gelule xenical 20 mg clomid online 150 mg wellbutrin sr buspar or zoloft diflucan prescription australia celebrex capsule 100 mg lisinopril 2.5mg tablets levitra cost mesico images of buspar doxycycline costs uk clomid pharmacy nz pills wc viagra viagra online uae 500 mg cipro dosage celebrex 200 mg arthritis viagra customs uk buy 500 mg lasix celebrex 200mg online kamagra uk pharmacy nexium canada pharmacy buspar and inderal buspar discussion board viagra muscle aches buspar and ptsd mg wellbutrin xl buy viagra jhb viagra price kroger viagra price israel nexium generic us lasix 20mg sale buspar brain shocks using cipro 500mg viagra history drug cipro 4 generic viagra online nz metformin ratio 1000mg cialis 20mg costco wellbutrin xl buy viagra kopen india buy zithromax iv levitra fast delivery metformin er 500 price zoloft confusion disorientation 15mg buspar clomid without af zithromax cream price pharmacy cost viagra cialis 5mg dosage celebrex color pill order nexium 40mg buspar kidney zithromax 200mg 5ml houston area viagra hydrochlorothiazide cost 25mg nolvadex sale com buy viagra sukhumvit cytotec 200 mg lahore online viagra rx 400 mg synthroid buy clomid medication viagra falls usa clomid plus hcg buspar plus zoloft viagra wonder drug cialis rush delivery tetracycline cheap lisinopril related drugs celebrex coupons discounts cytotec online kaufen strattera drug zithromax online overnight levitra what mgs cialis products india Cialis 20mg USA canadian viagra mastercard doxycycline 100mg purchase kamagra uk germany cialis canada drugmart viagra 50 mg cheap kamagra brausetabletten erfahrungen indian viagra nepal strattera 60 mg precio zoloft strattera together buying viagra pens glucophage 1000 mg farmaco vegetal viagra 120 mg indian viagra tablet viagra sale of nausea from wellbutrin gabapentin zoloft together cialis 002 online augmentin adulte 500 mg cialis 5mg costs lasix tablets uses levitra canada iui clomid cost cialis prescription repeat prednisone sinusitis treatment clomid tablets dosage levitra de 100 mg 4 days without synthroid cipro 500 mg muadili viagra generico efeitos viagra online funziona phenergan and tinnitus cialis 25 mg nuspojave price viagra online whats 100mg viagra farmacia online clomid metformin cost philippines viagra 150 mgrms buspar ibuprofen cost viagra cialis pastilla prednisone 5mg cutting viagra pill augmentin prospect 875 mg erythromycin susceptible bacteria viagra prospecto pfizer doxycycline online buy prednisone versus prednisolone viagra buy toronto viagra pfizer instructions actoplus metformin coupon doxycycline ivf cost generic lexapro costs iskustva sa nexium 400 mg of diflucan buspar binge eating red cialis 200mg strattera 10 mg used vitex versus clomid viagra plus review comprare cialis india metformin causing hunger lexapro tablets 10mg what causes tetracycline uso cytotec colombia reussite avec clomid augmentin suspension label uk wholesale kamagra augmentin dosage sinus kamagra tablete indija zoloft dosage 100 mg canadian cialis 5mg metformin format 500 mg glucophage 1000 mg beipackzettel buspar official website buspar cold turkey daily cialis 2.5 canada prednisone 5mg biogaran canadaian generic viagra strattera causing drowsiness doxycycline acne 100 mg nexium fda drugs buspar bestellen forum generic levitra viagra pill id buspar numb lips cialis pricetesco cialis 36 hour online dcheap 5 mg cialis buy online nolvadex 604 celebrex nyquil together nolvadex 20 mg tablet 5mg cialis urine buspar buspirone medication greenstone generic valtrex doxycycline malaria canada wellbutrin shortage canada 3 5mg of cialis cialis cheap cost purchase augmentin online cialis 20 mg online levitra professional buy buspar website buy cytotec australia diflucan 100 mg tablet 05mg propecia use viagra cialis kamagra directions use strattera drug withdrawal lasix tablet 20 mg nexium versus generic viagra buyonline cialis generico 40 mg levitra 20 mg polska buspar et insomnie lexapro causing tinnitus zovirax online prescription cialis drug study levitra 5 mg opinioni order diflucan wean off buspar strattera versus effexor viagra sale india celebrex 200mg pills nexium price uk zovirax tabletten gravid viagra generico 150 mg valtrex price us enterococcus species cipro buy phenergan 25mg cialis costco price synthroid generic pill valtrex generic comparison cialis 500 mg generic cytotec tabletas 200 mg using zovirax cream discount viagra sales buspar prescribed for buspar bioavailability propecia dangerous drug cialis online kaufen propecia drug interactions brand 5mg cialis cialis price drop buy Cialis 60 Tabs discount cialis prices doxycycline succinate 25 mg propecia 1mg discount buy viagra luxembourg buy zithromax fast difference generic cialis viagra uk lloyds order cheap viagra augmentin 500mg 125 mg diflucan 400 mg cialis 100 mmg zovirax suspension dose cheap zoloft 100 mg cialis prescriptions lexapro 15 mg anxiety kamagra 100mg malay diflucan 150 mg beipackzettel is lasix dangerous 25mg zoloft withdrawal cialis generic prices zovirax suspension packungsbeilage online cialis sale walmart pharmacy diflucan propranolol er tablets strattera generic availability lexapro 5 mg enough cipro muscle tears celebrex annual sales australia online viagra levitra prices increase 2013 buspar libido buspar bivirkninger novo prednisone drug propecia vellus hair remedio propranolol 40mg kamagra plus cheap drug named prednisone nonprescription viagra pill id zoloft doxycycline uses women order cialis generic zovirax uk price cipro 750 mg dosage xenical bikin kurus cialis india thailand lorazepam with buspar xenical nz price using viagra black tetracycline suspension dosage nolvadex pct buy express generic cialis celebrex equivalent generic staphylococcus epidermidis cipro 90mg prednisone dose zoloft 5 omg hydrochlorothiazide 12.5 mg cap drug prices lisinopril cheap kamagra usa viagra wholesale canada lasix and nausea zoloft and robitussin zovirax tablet 400mg cipro trus bx levitra 20mg vardenafil propecia wholesale cialis tablete cenovnik cialis cheap egypt buspar dogs prednisone muscle pain hydrochlorothiazide 12.5 mg caps nolvadex 20 mg pills nexium alcohol use zithromax sale 1g viagra 800mg levitra orodispersibleuk viagra orders canada prednisone 10mg dogs kamagra brausetabletten forum viagra 500mg cheap metformin sales us amoxil 1g uk cytotec pour residus chewable viagra 100 mg generic viagra jel professional levitra pills usa viagra kullanimi lasix foglio illustrativo nexium ppi drug cialis 2.5mg price kamagra 100mg price viagra 50 mg vs 100 metformin 500 mg for buy nolvedex clomid periactin cost cialis prescription toronto cialis price usa clomid e lupus propecia male menopause buying doxycycline 100mg lexapro 10 mg price lexapro cost philippines viagra 100mg us cytotec pfizer costo precio lasix 40 mg usual dosage diflucan wellbutrin 150 mg absetzen nexium causes diarrhea levitra mauritius cerco viagra generico augmentin lupus buspar anxiety medicine walgreens propecia discount viagra drug insert viagra cost canadian olanzapine fluoxetine price propecia uk cheapest obat nexium 20 mg lisinopril cost costco propranolol movement disorders cephalexin plus bactrim zovirax drugstore com generic wellbutrin wpi 3332 cialis prescription latin thuoc propecia 1mg levitra kaufen paypal xenical 120 mg prospect buy strattera us teenage viagra prescriptions propecia fenesteride 1 mg cialis soft Canada clomid prescription help australia pharmacy viagra viagra delivery viagra 100mg pret ovulation nausea clomid price of doxycycline viagra mastercard buy levitra 10 mg nedir zoloft vieroitusoireet lexapro 10 mg api phenergan tablets uses tesco viagra prescriptions lasix 20 mg tablets doxycycline medlineplus cheap viagra sample celebrex monthly cost viagra 200mg paypal lasix pill description trust pharmacy cialis cialis took 20mg cialis using poppers nolvadex 20mg testeron viagra gold uk linee autobus cipro cytotec microgram tablets strattera 25 mg 78 cents viagra and purchase erythromycin causing vomiting metformin piller cialis canada price buying online propecia cheap kamagra pills viagra pills samples buspar and irritability xenical indian cheap cialis 2.5mg augmentin 125 mg chewable wlamart pharmacy cialis diflucan thrush flovent buying zovirax cream levitra 5 mg preis buspar sore muscles cipro 500mg bid zoloft zkusenosti mercury drugs doxycycline uk viagra prescriptions diflucan 100mg online propecia india augmentin antybiotyk 625 mg manila generic cialis zithromax 500 mg filmtabl