src/util/channel.h

   1 /*********************                                                        */
   2 /*! \file channel.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project but is excluded from the
   8  ** standard CVC4 licensing because it is a derivative work of
   9  ** circular_buffer.hpp in the BOOST 1.46.1 distribution.
  10  ** Thus this file is covered by the Boost Software License, version 1.0.
  11  ** See below.
  12  **
  13  ** The combined work is:
  14  **   Copyright (c) 2009-2014  New York University and The University of Iowa
  15  **   Copyright (c) 2003-2008  Jan Gaspar
  16  **
  17  ** \brief [[ Add one-line brief description here ]]
  18  **
  19  ** [[ Add lengthier description here ]]
  20  ** \todo document this file
  21  **/
  22
  23 #include "cvc4_public.h"
  24
  25 #ifndef __CVC4__CHANNEL_H
  26 #define __CVC4__CHANNEL_H
  27
  28 #include <boost/circular_buffer.hpp>
  29 #include <boost/thread/mutex.hpp>
  30 #include <boost/thread/condition.hpp>
  31 #include <boost/thread/thread.hpp>
  32 #include <boost/call_traits.hpp>
  33 #include <boost/progress.hpp>
  34 #include <boost/bind.hpp>
  35
  36 namespace CVC4 {
  37
  38 template <typename T>
  39 class CVC4_PUBLIC SharedChannel {
  40 private:
  41   int d_maxsize;                // just call it size?
  42 public:
  43   SharedChannel() {}
  44   SharedChannel(int maxsize) : d_maxsize(maxsize) {}
  45   virtual ~SharedChannel() {}
  46
  47   /* Tries to add element and returns true if successful */
  48   virtual bool push(const T&) = 0;
  49
  50   /* Removes an element from the channel */
  51   virtual T pop() = 0;
  52
  53   /* */
  54   virtual bool empty() = 0;
  55
  56   /* */
  57   virtual bool full() = 0;
  58 };/* class SharedChannel<T> */
  59
  60 /*
  61 This code is from
  62
  63 http://live.boost.org/doc/libs/1_46_1/libs/circular_buffer/doc/circular_buffer.html#boundedbuffer
  64
  65 and is covered by the Boost Software License, version 1.0.
  66 */
  67 template <typename T>
  68 class CVC4_PUBLIC SynchronizedSharedChannel : public SharedChannel<T> {
  69 public:
  70   typedef boost::circular_buffer<T> container_type;
  71   typedef typename container_type::size_type size_type;
  72   typedef typename container_type::value_type value_type;
  73   typedef typename boost::call_traits<value_type>::param_type param_type;
  74
  75   explicit SynchronizedSharedChannel(size_type capacity) : m_unread(0), m_container(capacity) {}
  76
  77   bool push(param_type item){
  78   // param_type represents the "best" way to pass a parameter of type value_type to a method
  79
  80     boost::mutex::scoped_lock lock(m_mutex);
  81     m_not_full.wait(lock, boost::bind(&SynchronizedSharedChannel<value_type>::is_not_full, this));
  82     m_container.push_front(item);
  83     ++m_unread;
  84     lock.unlock();
  85     m_not_empty.notify_one();
  86     return true;
  87   }//function definitions need to be moved to cpp
  88
  89   value_type pop(){
  90     value_type ret;
  91     boost::mutex::scoped_lock lock(m_mutex);
  92     m_not_empty.wait(lock, boost::bind(&SynchronizedSharedChannel<value_type>::is_not_empty, this));
  93     ret = m_container[--m_unread];
  94     lock.unlock();
  95     m_not_full.notify_one();
  96     return ret;
  97   }
  98
  99
 100   bool empty() { return not is_not_empty(); }
 101   bool full() { return not is_not_full(); }
 102
 103 private:
 104   SynchronizedSharedChannel(const SynchronizedSharedChannel&);              // Disabled copy constructor
 105   SynchronizedSharedChannel& operator = (const SynchronizedSharedChannel&); // Disabled assign operator
 106
 107   bool is_not_empty() const { return m_unread > 0; }
 108   bool is_not_full() const { return m_unread < m_container.capacity(); }
 109
 110   size_type m_unread;
 111   container_type m_container;
 112   boost::mutex m_mutex;
 113   boost::condition m_not_empty;
 114   boost::condition m_not_full;
 115 };/* class SynchronizedSharedChannel<T> */
 116
 117 }/* CVC4 namespace */
 118
 119 #endif /* __CVC4__CHANNEL_H */